lesson2

To play this document inside your browser use ALT-N and ALT-P. You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

From elpi Require Import elpi.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Roadmap of the second lesson

Playing with basic arithmetics

Order
Division
Primality

Reminder

Natural numbers

Check nat.
(* nat : Set *)

Print nat.
(* Inductive nat : Set :=
   O : nat | S : nat -> nat *)

Check O.
(* 0 : nat *)

Check S O.
(* 1 : nat *)

Check S (S O).
(* 2 : nat *)

Check 2.+1.
(* 3 : nat *)

Set Printing All.
Check 4.
(* S (S (S O)) : nat *)

Unset Printing All.
Check 5.
(* 5 : nat *)

Reminder

Proof by case


Goal forall (P : pred nat), 
     P 0 -> (forall n, P n.+1) -> forall n, P n.
Proof.
move=> P HP0 HPS n.
case: n => [|n].
  exact: HP0.
by apply: HPS.
Qed.

Reminder

Proof by induction


Goal forall (P : pred nat), 
     P 0 -> (forall n, P n -> P n.+1) -> forall n, P n.
Proof.
move=> P HP0 HPS n.
elim: n => [|n IH].
  exact: HP0.
by apply: HPS.
Qed.

Reminder

Eq type


Check eqn.
(* eqn : nat -> nat -> bool *)

Print eqn.
(* fix eqn (m n : nat) {struct m} : bool :=
   match m with ... end. *)

Compute 1 == 1.
(* true : bool *)

Compute 2 == 3.
(* false : bool *)

Goal forall m n, m.+1 == n.+1 -> m == n.
Proof.
move=> m n mEn.
exact: mEn.
Qed.

Natural numbers

Addition


Check addn.
(* addn : nat -> nat -> nat *)

Check addn 2 3.
(* 2 + 3 : nat *)

Compute 2 + 3.
(* 5 : nat *)

Goal forall m n, m.+1 + n = (m + n).+1.
Proof.
move=> m n.
by [].
Qed.

Search (_.+1 + _ = _.+1) in ssrnat.
(*
add1n: forall n : nat, 1 + n = n.+1
addSn: forall m n : nat, m.+1 + n = (m + n).+1
add2n: forall m : nat, 2 + m = m.+2
add3n: forall m : nat, 3 + m = m.+3
add4n: forall m : nat, 4 + m = m.+4
*)

Goal forall m n, m + n.+1 = (m + n).+1.
Proof.
move=> m n.
elim: m => [|m IH].
  by [].
rewrite !addSn.
rewrite IH.
by [].
Qed.

Search (_ + _.+1 = _.+1) in ssrnat.
(*
addn1: forall n : nat, n + 1 = n.+1
addnS: forall m n : nat, m + n.+1 = (m + n).+1
addn2: forall m : nat, m + 2 = m.+2
addn3: forall m : nat, m + 3 = m.+3
addn4: forall m : nat, m + 4 = m.+4
*)

Search (_.+1 + _ = _ + _.+1) in ssrnat.
(* addSnnS: forall m n : nat, m.+1 + n = m + n.+1*)

Natural Numbers

Subtraction


Check subn.
(* subn : nat -> nat -> nat *)

Check subn 3 2.
(* 3 - 2 : nat *)

Compute 3 - 2.
(* 1 : nat *)

Compute 3 - 4.
(* 0 : nat *)

Goal forall n, 0 - n = 0.
Proof.
move=> n.
by [].
Qed.

Search left_zero subn in ssrnat.
(* sub0n: left_zero 0 subn *)

Goal forall n, n - 0 = n.
Proof.
case => [|n].
- by [].
by [].
Qed.

Search (_.+1 - _.+1 = _) in ssrnat.
(* sub0n: left_zero 0 subn *)

Natural Numbers

Order


Check leq.
(* nat -> nat -> bool *)

Check 0 <= 2.
(* 0 <= 2 : bool *)

Compute (0 <= 2).
(* true : bool *)

Print leq.
(* leq = fun m n : nat => m - n == 0
     : nat -> nat -> bool
*)

One definition several notations


Goal forall m n, m >= n -> n <= m.
Proof.
by [].
Qed.

Goal forall m n, m.+1 <= n -> m < n.
Proof.
by [].
Qed.

Goal forall n, n <= n.+1.
Proof.
elim=> [|n IH].
  by [].
exact: IH.
Qed.

Search (?_1 <= ?_1.+1) in ssrnat.
(* eqnSn: forall n : nat, n <= n.+1 *)

Reflexivity


Search (?_1 <= ?_1) in ssrnat.
(*
leqnn: forall n : nat, n <= n
ltnSn: forall n : nat, n < n.+1
*)

Antisymmetry


Search (~~ _) (_ <= _) in ssrnat.
(*
ltnNge: forall m n : nat, (m < n) = ~~ (n <= m)
leqNgt: forall m n : nat, (m <= n) = ~~ (n < m)
lt0n_neq0: forall [n : nat], 0 < n -> n != 0
ltnNleqif: forall [x y : nat] [C : bool], x <= y ?= iff ~~ C -> (x < y) = C
ltn_leqif: forall [a b : nat] [C : bool], a <= b ?= iff C -> (a < b) = ~~ C
lt0n: forall n : nat, (0 < n) = (n != 0)
eqn0Ngt: forall n : nat_eqType, (n == 0) = ~~ (0 < n)
contraNleq: forall [b : bool] [m n : nat], (n < m -> b) -> ~~ b -> m <= n
contra_leqT: forall [b : bool] [m n : nat], (~~ b -> m < n) -> n <= m -> b
contra_ltnT: forall [b : bool] [m n : nat], (~~ b -> m <= n) -> n < m -> b
contraTleq: forall [b : bool] [m n : nat], (n < m -> ~~ b) -> b -> m <= n
contraNltn: forall [b : bool] [m n : nat], (n <= m -> b) -> ~~ b -> m < n
contra_ltnN: forall [b : bool] [m n : nat], (b -> m <= n) -> n < m -> ~~ b
contraTltn: forall [b : bool] [m n : nat], (n <= m -> ~~ b) -> b -> m < n
contra_leqN: forall [b : bool] [m n : nat], (b -> m < n) -> n <= m -> ~~ b
*)

Search (_ == _ = _) (_ <= _) in ssrnat.
(*
subn_eq0: forall m n : nat, (m - n == 0) = (m <= n)
eqn0Ngt: forall n : nat_eqType, (n == 0) = ~~ (0 < n)
eqn_leq: forall m n : nat_eqType, (m == n) = (m <= n <= m)
ltn_eqF: forall [m n : nat], m < n -> (m == n) = false
gtn_eqF: forall [m n : nat], m < n -> (n == m) = false
neq0_lt0n: forall [n : nat_eqType], (n == 0) = false -> 0 < n
expn_eq0: forall m e : nat, (m ^ e == 0) = (m == 0) && (0 < e)
eqn_pmul2l: forall [m n1 n2 : nat], 0 < m -> (m * n1 == m * n2) = (n1 == n2)
eqn_exp2r: forall (m n : nat) [e : nat], 0 < e -> (m ^ e == n ^ e) = (m == n)
eqn_pmul2r: forall [m n1 n2 : nat], 0 < m -> (n1 * m == n2 * m) = (n1 == n2)
eqn_exp2l:
  forall [m : nat] (n1 n2 : nat), 1 < m -> (m ^ n1 == m ^ n2) = (n1 == n2)
*)

Transitivity


Search nat "trans" in ssrnat.
(*
leq_trans: forall [n m p : nat], m <= n -> n <= p -> m <= p
leqif_trans:
  forall [m1 m2 m3 : nat] [C12 C23 : bool],
  m1 <= m2 ?= iff C12 -> m2 <= m3 ?= iff C23 -> m1 <= m3 ?= iff C12 && C23
leq_ltn_trans: forall [n m p : nat], m <= n -> n < p -> m < p
ltn_trans: forall [n m p : nat], m < n -> n < p -> m < p
*)

Goal forall m n p, m < n -> n <= p -> m < p.
Proof.
move=> m n p.
have trans := leq_trans.
have trans_Sm_n := leq_trans (_ : m < n) (_ : n <= p).
by [].
Qed.

Goal forall (P : pred nat), 
      P 0 ->
      (forall m,  (forall n, n <= m -> P n) -> P m.+1) ->
      (forall m, P m).
Proof.
move=> P HC IHs m.
move: (leqnn m).
move: {-2}m.
elim: m => [|m IH].
  by case.
case=> // n nLm.
apply: IHs => k kLn.
apply: IH.
apply: leq_trans kLn nLm.
Qed.

Goal forall a b c,
   a < b -> b < c -> a <= c.
Proof.
move=> a b c aLb bLc.
apply: leq_trans (_ : b <= _).
  by apply: ltnW.
by apply: ltnW.
Qed.

Proof by case


Goal forall (m : nat) (n : nat) (P : nat -> bool), 
   (n <= m -> P n) -> (m < n -> P n) -> P n.
Proof.
move=> m n P LP GP.
case: (leqP n m).
  by apply: LP.
by apply: GP.
Qed.

Goal forall (m : nat) (n : nat) (P : nat -> bool), 
   (n < m -> P n) -> (m < n -> P n) -> (n = m -> P n) -> P n.
Proof.
move=> m n P LP GP EP.
case: (ltngtP n m).
- by apply: LP.
- by apply: GP.
by apply: EP.
Qed.

Check leq_eqVlt.
(* leq_eqVlt
         : forall m n : nat, (m <= n) = (m == n) || (m < n)
*)

Goal forall (P : pred nat) m n, P n ->
    (m < n -> P m) -> m <= n -> P m.
Proof.
move=> P m n Pn PL.
rewrite leq_eqVlt.
move=> /orP[|].
  move/eqP->.
  by [].
exact: PL.
Qed.

Goal forall (P : pred nat) m n, P n ->
    (m < n -> P m) -> m <= n -> P m.
Proof.
move=> P m n Pn GP.
case: ltngtP.
- move=> mLn _.
  by apply: GP.
- by [].
move=> -> _.
exact: Pn.
Qed.

Addition


Search (_ <= _ + _) in ssrnat.
(*
leq_addr: forall m n : nat, n <= n + m
leq_addl: forall m n : nat, n <= m + n
leq_add2r: forall p m n : nat, (m + p <= n + p) = (m <= n)
leq_add2l: forall p m n : nat, (p + m <= p + n) = (m <= n)
ltn_addl: forall [m n : nat] (p : nat), m < n -> m < p + n
leq_subLR: forall m n p : nat, (m - n <= p) = (m <= n + p)
ltn_addr: forall [m n : nat] (p : nat), m < n -> m < n + p
ltn_add2r: forall p m n : nat, (m + p < n + p) = (m < n)
ltn_add2l: forall p m n : nat, (p + m < p + n) = (m < n)
leq_add:
  forall [m1 m2 n1 n2 : nat], m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2
addn_gt0: forall m n : nat, (0 < m + n) = (0 < m) || (0 < n)
ltn_subLR: forall [m n : nat] (p : nat), n <= m -> (m - n < p) = (m < n + p)
ltn_psubLR: forall (m n : nat) [p : nat], 0 < p -> (m - n < p) = (m < n + p)
*)

Goal forall m n, n <= m -> n.*2 <= m + n.
Proof.
move=> m n nLm.
rewrite -addnn.
rewrite leq_add2r.
by [].
Qed.

Multiplication


Search  _ (_ <= _ * _) in ssrnat.
(*
leq_pmulr: forall (m : nat) [n : nat], 0 < n -> m <= m * n
leq_pmull: forall (m : nat) [n : nat], 0 < n -> m <= n * m
leq_mul:
  forall [m1 m2 n1 n2 : nat], m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2
ltn_Pmull: forall [m n : nat], 1 < n -> 0 < m -> m < n * m
ltn_Pmulr: forall [m n : nat], 1 < n -> 0 < m -> m < m * n
muln_gt0: forall m n : nat, (0 < m * n) = (0 < m) && (0 < n)
ltn_mul: forall [m1 m2 n1 n2 : nat], m1 < n1 -> m2 < n2 -> m1 * m2 < n1 * n2
leq_pmul2l: forall [m n1 n2 : nat], 0 < m -> (m * n1 <= m * n2) = (n1 <= n2)
leq_pmul2r: forall [m n1 n2 : nat], 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2)
leq_mul2r: forall m n1 n2 : nat, (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2)
leq_mul2l: forall m n1 n2 : nat, (m * n1 <= m * n2) = (m == 0) || (n1 <= n2)
ltn_mul2l: forall m n1 n2 : nat, (m * n1 < m * n2) = (0 < m) && (n1 < n2)
ltn_mul2r: forall m n1 n2 : nat, (n1 * m < n2 * m) = (0 < m) && (n1 < n2)
ltn_pmul2r: forall [m n1 n2 : nat], 0 < m -> (n1 * m < n2 * m) = (n1 < n2)
ltn_pmul2l: forall [m n1 n2 : nat], 0 < m -> (m * n1 < m * n2) = (n1 < n2)
*)

Goal forall m n, n <= m -> n ^ 2 <= m * n.
Proof.
move=> m n nLm.
rewrite -mulnn.
rewrite leq_mul2r.
rewrite nLm.
rewrite orbT.
by [].
Qed.

Conditional comparison


Search (_ <= _ ?= iff _) (_ && _) in ssrnat.
(*
eqif_trans:
  forall [m1 m2 m3 : nat] [C12 C23 : bool],
  m1 <= m2 ?= iff C12 -> m2 <= m3 ?= iff C23 -> m1 <= m3 ?= iff C12 && C23
leqif_add:
  forall [m1 n1 : nat] [C1 : bool] [m2 n2 : nat] [C2 : bool],
  m1 <= n1 ?= iff C1 ->
  m2 <= n2 ?= iff C2 -> m1 + m2 <= n1 + n2 ?= iff C1 && C2
leqif_mul:
  forall [m1 n1 : nat] [C1 : bool] [m2 n2 : nat] [C2 : bool],
  m1 <= n1 ?= iff C1 ->
  m2 <= n2 ?= iff C2 -> m1 * m2 <= n1 * n2 ?= iff (n1 * n2 == 0) || C1 && C2
*)

Natural Numbers

Division


Check (modn 21 2).
(* 21  2 : nat *)

Compute 21 %% 2.
(* 1 : nat *)

Check (divn 21 2).
(* 21 *)

Compute 21 %/ 2.
(* 10 : nat *)

Check (dvdn 2 21).

Compute 2 %| 21.

Print dvdn.
(*
dvdn = fun d m : nat => m %% d == 0
	 : nat -> nat -> bool
*)

Search (_ %| _ + _) in div.
(* 
dvdn_add: forall [d m n : nat], d %| m -> d %| n -> d %| m + n
dvdn_add_eq: forall [d m n : nat], d %| m + n -> (d %| m) = (d %| n)
dvdn_addl: forall [n d : nat] (m : nat), d %| n -> (d %| m + n) = (d %| m)
dvdn_addr: forall [m d : nat] (n : nat), d %| m -> (d %| m + n) = (d %| n)
Bezoutl:
  forall [m : nat] (n : nat),
  0 < m -> {a : nat | a < m & m %| gcdn m n + a * n}
Bezoutr:
  forall (m : nat) [n : nat],
  0 < n -> {a : nat | a < n & n %| gcdn m n + a * m}
*)

Search ((_ + _) %/ _) in div.
(*
divnDr:
  forall (m : nat) [n d : nat], d %| n -> (m + n) %/ d = m %/ d + n %/ d
divnDl:
  forall [m : nat] (n : nat) [d : nat],
  d %| m -> (m + n) %/ d = m %/ d + n %/ d
leq_divDl: forall p m n : nat, (m + n) %/ p <= m %/ p + n %/ p + 1
divnDMl: forall (q m : nat) [d : nat], 0 < d -> (m + q * d) %/ d = m %/ d + q
divnMDl: forall (q m : nat) [d : nat], 0 < d -> (q * d + m) %/ d = q + m %/ d
divnD:
  forall (m n : nat) [d : nat],
  0 < d -> (m + n) %/ d = m %/ d + n %/ d + (d <= m %% d + n %% d)
*)

Search (?_1 %/ ?_1) in div.
(* divnn: forall d : nat, d %/ d = (0 < d) *)

Compute 0 %/ 0.
(* 0 : nat *)

Search (_ %| _ * _) in div.
(* 
dvdn_mulr: forall [d m : nat] (n : nat), d %| m -> d %| m * n
dvdn_mull: forall [d : nat] (m : nat) [n : nat], d %| n -> d %| m * n
dvdn_mul:
  forall [d1 d2 m1 m2 : nat], d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2
Gauss_dvdl:
  forall [m : nat] (n : nat) [p : nat],
  coprime m p -> (m %| n * p) = (m %| n)
Gauss_dvdr:
  forall [m n : nat] (p : nat), coprime m n -> (m %| n * p) = (m %| p)
dvdn_pmul2l: forall [p d m : nat], 0 < p -> (p * d %| p * m) = (d %| m)
dvdn_pmul2r: forall [p d m : nat], 0 < p -> (d * p %| m * p) = (d %| m)
dvdn_divLR:
  forall [p d : nat] (m : nat),
  0 < p -> p %| d -> (d %/ p %| m) = (d %| m * p)
*)

Search ((_ * _) %/ _) in div.
(*
divnA: forall (m : nat) [n p : nat], p %| n -> m %/ (n %/ p) = (m * p) %/ n
muln_divA:
  forall [d : nat] (m : nat) [n : nat], d %| n -> m * (n %/ d) = (m * n) %/ d
divn_mulAC: forall [d m : nat] (n : nat), d %| m -> m %/ d * n = (m * n) %/ d
mulKn: forall (m : nat) [d : nat], 0 < d -> (d * m) %/ d = m
mulnK: forall (m : nat) [d : nat], 0 < d -> (m * d) %/ d = m
divnMl: forall [p m d : nat], 0 < p -> (p * m) %/ (p * d) = m %/ d
divnMr: forall [p m d : nat], 0 < p -> (m * p) %/ (d * p) = m %/ d
*)

Natural Numbers

Odd


Compute odd 4.
(* false : bool *)

Compute odd 5.
(* true : bool *)

Print odd.
(* 
odd = 
fix odd (n : nat) : bool :=
  match n with
  | 0 => false
  | n'.+1 => ~~ odd n'
  end
         : nat -> bool
*)

Search odd (_ %% _) in div.
(* 
modn2: forall m : nat, m %% 2 = odd m
odd_mod: forall (m : nat) [d : nat], odd d = false -> odd (m %% d) = odd m
*)

Natural Numbers

Gcd and Lcm


Compute gcdn 42 49.
(* 7 : nat *)

Compute lcmn 42 49.
(* 294 : nat *)

Search gcdn lcmn in div.
(* 
muln_lcm_gcd: forall m n : nat, lcmn m n * gcdn m n = m * n
*)

Search gcdn (_ * _) in div.
(* 
gcdnMr: forall n m : nat, gcdn n (n * m) = n
gcdnMl: forall n m : nat, gcdn n (m * n) = n
muln_lcm_gcd: forall m n : nat, lcmn m n * gcdn m n = m * n
gcdnMDl: forall k m n : nat, gcdn m (k * m + n) = gcdn m n
muln_divCA_gcd: forall n m : nat, n * (m %/ gcdn n m) = m * (n %/ gcdn n m)
Gauss_gcdl:
  forall [p : nat] (m : nat) [n : nat],
  coprime p n -> gcdn p (m * n) = gcdn p m
Gauss_gcdr:
  forall [p m : nat] (n : nat), coprime p m -> gcdn p (m * n) = gcdn p n
Bezoutl:
  forall [m : nat] (n : nat),
  0 < m -> {a : nat | a < m & m %| gcdn m n + a * n}
Bezoutr:
  forall (m : nat) [n : nat],
  0 < n -> {a : nat | a < n & n %| gcdn m n + a * m}
EgcdnSpec:
  forall [m n km kn : nat],
  km * m = kn * n + gcdn m n -> kn * gcdn m n < m -> egcdn_spec m n (km, kn)
*)

Natural Numbers

Coprime & Prime


Check coprime.
(* coprime : nat -> nat -> bool *)

Compute coprime 3 5.
(* true : bool *)

Compute coprime 21 7.
(* false : true *)

Print coprime.
(* 
coprime = fun m n : nat => gcdn m n == 1
         : nat -> nat -> bool
*)

Search coprime (_ %| _) in div prime.
(*
coprime_dvdr: forall [m n p : nat], m %| n -> coprime p n -> coprime p m
coprime_dvdl: forall [m n p : nat], m %| n -> coprime n p -> coprime m p
prime_coprime:
  forall [p : nat] (m : nat), prime p -> coprime p m = ~~ (p %| m)
Gauss_dvdr:
  forall [m n : nat] (p : nat), coprime m n -> (m %| n * p) = (m %| p)
Gauss_dvdl:
  forall [m : nat] (n : nat) [p : nat],
  coprime m p -> (m %| n * p) = (m %| n)
Gauss_dvd:
  forall [m n : nat] (p : nat),
  coprime m n -> (m * n %| p) = (m %| p) && (n %| p)
*)

Check prime.
(* prime : nat -> bool *)

Compute prime 21.
(* false : bool *)

Compute prime 22.
(* false : bool *)

Compute prime 23.
(* true : bool *)

Print prime.
(*
prime = 
fun p : nat =>
match prime_decomp p with
| [:: (_, 1)]  => true
| _ => false
end     : nat -> bool
*)

Compute primes 21.
(* [:: 3, 7] : seq nat *)
Compute primes 22.
(* [:: 2; 11] : seq nat *)

Compute primes 23.
(* [:: 23] : seq nat *)

Check primeP.
(* 
primeP
	 : reflect (1 < ?p /\ (forall d : nat, d %| ?p -> (d == 1) || (d == ?p)))
         (prime ?p)
*)

Goal prime 2.
Proof.
apply/primeP.
split.
  by [].
move=> d.
case: d.
  by [].
case.
  by [].
by case.
Qed.

Search prime (_ %| _) in div prime.
(*
Euclid_dvd1: forall [p : nat], prime p -> (p %| 1) = false
prime_coprime:
  forall [p : nat] (m : nat), prime p -> coprime p m = ~~ (p %| m)
dvdn_prime2: forall [p q : nat], prime p -> prime q -> (p %| q) = (p == q)
pdivP: forall [n : nat], 1 < n -> {p : nat | prime p & p %| n}
Euclid_dvdM:
  forall (m n : nat) [p : nat],
  prime p -> (p %| m * n) = (p %| m) || (p %| n)
p'natE: forall [p : nat] (n : nat), prime p -> (p^').-nat n = ~~ (p %| n)
Euclid_dvdX:
  forall (m n : nat) [p : nat], prime p -> (p %| m ^ n) = (p %| m) && (0 < n)
dvdn_pfactor:
  forall [p : nat] (d n : nat),
  prime p -> reflect (exists2 m : nat, m <= n & d = p ^ m) (d %| p ^ n)
lognE:
  forall p m : nat,
  logn p m =
  (if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0)
pfactor_dvdn:
  forall [p : nat] (n : nat) [m : nat],
  prime p -> 0 < m -> (p ^ n %| m) = (n <= logn p m)
prime_nt_dvdP:
  forall [d : nat_eqType] [p : nat],
  prime p -> d != 1 -> reflect (d = p) (d %| p)
pnatP:
  forall (pi : nat_pred) [n : nat],
  0 < n ->
  reflect (forall p : nat, prime p -> p %| n -> p \in pi) (pi.-nat n)
mem_primes:
  forall (p : nat_eqType) (n : nat),
  (p \in primes n) = [&& prime p, 0 < n & p %| n]
primePn:
  forall {n : nat},
  reflect (n < 2 \/ (exists2 d : nat, 1 < d < n & d %| n)) (~~ prime n)
logn_count_dvd:
  forall [p : nat] (n : nat),
  prime p -> logn p n = \sum_(1 <= k < n) (p ^ k %| n)
primePns:
  forall {n : nat},
  reflect (n < 2 \/ (exists p : nat, [/\ prime p, p ^ 2 <= n & p %| n]))
	(~~ prime n)
primeP:
  forall {p : nat},
  reflect (1 < p /\ (forall d : nat, d %| p -> xpred2 1 p d)) (prime p)
Euclid_dvd_prod:
  forall [I : Type] (r : seq I) (P : pred I) (f : I -> nat) [p : nat],
  prime p ->
  (p %| \prod_(i <- r | P i) f i) = \big[orb/false]_(i <- r | P i) (p %| f i)
mem_prime_decomp:
  forall [n : nat] [p e : nat_eqType],
  (p, e) \in prime_decomp n -> [/\ prime p, 0 < e & p ^ e %| n]
*)

Check logn.
(* logn : nat -> nat -> nat*)

Compute logn 3 8.
(* 0 : nat *)
Compute logn 3 9.
(* 2 : nat *)

Search logn in prime.
(* 
logn0: forall p : nat, logn p 0 = 0
logn1: forall p : nat, logn p 1 = 0
pfactor_dvdnn: forall p n : nat, p ^ logn p n %| n
logn_part: forall p m : nat, logn p m`_p = logn p m
logn_coprime: forall [p m : nat], coprime p m -> logn p m = 0
lognX: forall p m n : nat, logn p (m ^ n) = n * logn p m
p_part: forall p n : nat, n`_p = p ^ logn p n
pfactorK: forall [p : nat] (n : nat), prime p -> logn p (p ^ n) = n
pfactor_gt0: forall p n : nat, 0 < p ^ logn p n
ltn_logl: forall (p : nat) [n : nat], 0 < n -> logn p n < n
ltn_log0: forall [p n : nat], n < p -> logn p n = 0
logn_Gauss:
  forall [p m : nat] (n : nat), coprime p m -> logn p (m * n) = logn p n
pfactorKpdiv:
  forall [p : nat] (n : nat), prime p -> logn (pdiv (p ^ n)) (p ^ n) = n
logn_prime: forall (p : nat) [q : nat], prime q -> logn p q = (p == q)
logn_div:
  forall (p : nat) [m n : nat],
  m %| n -> logn p (n %/ m) = logn p n - logn p m
dvdn_leq_log:
  forall (p : nat) [m n : nat], 0 < n -> m %| n -> logn p m <= logn p n
prime_decompE:
  forall n : nat, prime_decomp n = [seq (p, logn p n) | p <- primes n]
eqn_from_log:
  forall [m n : nat], 0 < m -> 0 < n -> logn^~ m =1 logn^~ n -> m = n
logn_gt0: forall p n : nat, (0 < logn p n) = (p \in primes n)
lognE:
  forall p m : nat,
  logn p m =
  (if [&& prime p, 0 < m & p %| m] then (logn p (m %/ p)).+1 else 0)
logn_lcm:
  forall (p : nat) [m n : nat],
  0 < m -> 0 < n -> logn p (lcmn m n) = maxn (logn p m) (logn p n)
lognM:
  forall (p : nat) [m n : nat],
  0 < m -> 0 < n -> logn p (m * n) = logn p m + logn p n
logn_gcd:
  forall (p : nat) [m n : nat],
  0 < m -> 0 < n -> logn p (gcdn m n) = minn (logn p m) (logn p n)
pfactor_dvdn:
  forall [p : nat] (n : nat) [m : nat],
  prime p -> 0 < m -> (p ^ n %| m) = (n <= logn p m)
pfactor_coprime:
  forall [p n : nat],
  prime p -> 0 < n -> {m : nat | coprime p m & n = m * p ^ logn p n}
logn_count_dvd:
  forall [p : nat] (n : nat),
  prime p -> logn p n = \sum_(1 <= k < n) (p ^ k %| n)
totientE:
  forall [n : nat],
  0 < n -> totient n = \prod_(p <- primes n) (p.-1 * p ^ (logn p n).-1)
widen_partn:
  forall [m : nat] (pi : nat_pred) [n : nat],
  n <= m -> n`_pi = \prod_(0 <= p < m.+1 | p \in pi) p ^ logn p n
eq_partn_from_log:
  forall [m n : nat] [pi : nat_pred],
  0 < m -> 0 < n -> {in pi, logn^~ m =1 logn^~ n} -> m`_pi = n`_pi
*)