Library Ssreflect.div
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Euclidian division
Definition edivn_rec d := fix loop (m q : nat) {struct m} :=
if m - d is m'.+1 then loop m' q.+1 else (q, m).
Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
CoInductive edivn_spec (m d : nat) : nat * nat -> Type :=
EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).
Lemma edivnP : forall m d, edivn_spec m d (edivn m d).
Proof.
rewrite /edivn => m [|d] //=; rewrite -{1}[m]/(0 * d.+1 + m).
elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=; rewrite ltnS => le_mn.
rewrite subn_if_gt; case: ltnP => [// | le_dm].
rewrite -{1}(subnKC le_dm) -addSn addnA -mulSnr; apply: IHn.
apply: leq_trans le_mn; exact: leq_subr.
Qed.
Lemma edivn_eq : forall d q r, r < d -> edivn (q * d + r) d = (q, r).
Proof.
move=> d q r lt_rd; have d_gt0: 0 < d by exact: leq_trans lt_rd.
case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
wlog: q q' r r' / q <= q' by case (ltnP q q'); last symmetry; eauto.
rewrite leq_eqVlt; case: eqP => [-> _|_] /=; first by move/addnI->.
rewrite -(leq_pmul2r d_gt0); move/leq_add=> Hqr Eqr _; move/Hqr {Hqr}.
by rewrite addnS ltnNge mulSn -addnA Eqr addnCA addnA leq_addr.
Qed.
Definition divn m d := (edivn m d).1.
Notation "m %/ d" := (divn m d) (at level 40, no associativity) : nat_scope.
Definition modn_rec d := fix loop (m : nat) :=
if m - d is m'.+1 then loop m' else m.
Definition modn m d := if d > 0 then modn_rec d.-1 m else m.
Notation "m %% d" := (modn m d) (at level 40, no associativity) : nat_scope.
Notation "m = n %[mod d ]" := (m %% d = n %% d)
(at level 70, n at next level,
format "'[hv ' m '/' = n '/' %[mod d ] ']'") : nat_scope.
Notation "m == n %[mod d ]" := (m %% d == n %% d)
(at level 70, n at next level,
format "'[hv ' m '/' == n '/' %[mod d ] ']'") : nat_scope.
Notation "m <> n %[mod d ]" := (m %% d <> n %% d)
(at level 70, n at next level,
format "'[hv ' m '/' <> n '/' %[mod d ] ']'") : nat_scope.
Notation "m != n %[mod d ]" := (m %% d != n %% d)
(at level 70, n at next level,
format "'[hv ' m '/' != n '/' %[mod d ] ']'") : nat_scope.
Lemma modn_def : forall m d, m %% d = (edivn m d).2.
Proof.
rewrite /modn /edivn => m [|d] //=.
elim: m {-2}m 0 (leqnn m) => [|n IHn] [|m] q //=.
rewrite ltnS !subn_if_gt; case: (d <= m) => // le_mn.
by apply: IHn; apply: leq_trans le_mn; exact: leq_subr.
Qed.
Lemma edivn_def : forall m d, edivn m d = (m %/ d, m %% d).
Proof. by move=> m d; rewrite /divn modn_def; case edivn. Qed.
Lemma divn_eq : forall m d, m = m %/ d * d + m %% d.
Proof. by move=> m d; rewrite /divn modn_def; case edivnP. Qed.
Lemma div0n : forall d, 0 %/ d = 0. Proof. by case. Qed.
Lemma divn0 : forall m, m %/ 0 = 0. Proof. by []. Qed.
Lemma mod0n : forall d, 0 %% d = 0. Proof. by case. Qed.
Lemma modn0 : forall m, m %% 0 = m. Proof. by []. Qed.
Lemma divn_small : forall m d, m < d -> m %/ d = 0.
Proof. by move=> m d lt_md; rewrite /divn (edivn_eq 0). Qed.
Lemma divn_addl_mul : forall q m d, 0 < d -> (q * d + m) %/ d = q + m %/ d.
Proof.
move=> q m d d_gt0; rewrite {1}(divn_eq m d) addnA -muln_addl.
by rewrite /divn edivn_eq // modn_def; case: edivnP; rewrite d_gt0.
Qed.
Lemma mulnK : forall m d, 0 < d -> m * d %/ d = m.
Proof.
by move=> m d d_gt0; rewrite -[m * d]addn0 divn_addl_mul // div0n addn0.
Qed.
Lemma mulKn : forall m d, 0 < d -> d * m %/ d = m.
Proof. by move=> *; rewrite mulnC mulnK. Qed.
Lemma modn1 : forall m, m %% 1 = 0.
Proof. by move=> m; rewrite modn_def; case: edivnP => ? []. Qed.
Lemma divn1: forall m, m %/ 1 = m.
Proof. by move=> m; rewrite {2}(@divn_eq m 1) // modn1 addn0 muln1. Qed.
Lemma divnn : forall d, d %/ d = (0 < d).
Proof. by case=> // d; rewrite -{1}[d.+1]muln1 mulKn. Qed.
Lemma divn_pmul2l : forall p m d, p > 0 -> p * m %/ (p * d) = m %/ d.
Proof.
move=> p m d p_gt0; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
rewrite {2}/divn; case: edivnP; rewrite d_gt0 /= => q r ->{m} lt_rd.
rewrite muln_addr mulnCA divn_addl_mul; last by rewrite muln_gt0 p_gt0.
by rewrite addnC divn_small // ltn_pmul2l.
Qed.
Implicit Arguments divn_pmul2l [p m d].
Lemma divn_pmul2r : forall p m d, p > 0 -> m * p %/ (d * p) = m %/ d.
Proof. by move=> p m d p_gt0; rewrite -!(mulnC p) divn_pmul2l. Qed.
Implicit Arguments divn_pmul2r [p m d].
Lemma ltn_mod : forall m d, (m %% d < d) = (0 < d).
Proof. by move=> m [|d] //; rewrite modn_def; case: edivnP. Qed.
Lemma ltn_pmod : forall m d, 0 < d -> m %% d < d.
Proof. by move=> m d; rewrite ltn_mod. Qed.
Lemma leq_floor : forall m d, m %/ d * d <= m.
Proof. by move=> m d; rewrite {2}(divn_eq m d) leq_addr. Qed.
Lemma leq_mod : forall m d, m %% d <= m.
Proof. by move=> m d; rewrite {2}(divn_eq m d) leq_addl. Qed.
Lemma leq_div : forall m d, m %/ d <= m.
Proof. move=> m [|d] //; exact: leq_trans (leq_pmulr _ _) (leq_floor _ _). Qed.
Lemma ltn_ceil : forall m d, 0 < d -> m < (m %/ d).+1 * d.
Proof.
by move=> m d ? /=; rewrite {1}(divn_eq m d) -addnS mulSnr leq_add2l ltn_mod.
Qed.
Lemma ltn_divl : forall m n d, d > 0 -> (m %/ d < n) = (m < n * d).
Proof.
move=> m n d d_gt0; apply/idP/idP.
rewrite -(leq_pmul2r d_gt0); exact: leq_trans (ltn_ceil _ _).
rewrite !ltnNge -(@leq_pmul2r d n) //; apply: contra => le_nd_floor.
exact: leq_trans le_nd_floor (leq_floor _ _).
Qed.
Lemma leq_divr : forall m n d, d > 0 -> (m <= n %/ d) = (m * d <= n).
Proof. by move=> m n d d_gt0; rewrite leqNgt ltn_divl // -leqNgt. Qed.
Lemma ltn_Pdiv : forall m d, 1 < d -> 0 < m -> m %/ d < m.
Proof. by move=> m d d_gt1 m_gt0; rewrite ltn_divl ?ltn_Pmulr // ltnW. Qed.
Lemma divn_gt0 : forall d m, 0 < d -> (0 < m %/ d) = (d <= m).
Proof. by move=> d m d_gt0; rewrite leq_divr ?mul1n. Qed.
Lemma divn_divl : forall m n p, m %/ n %/ p = m %/ (n * p).
Proof.
move=> m [|n] [|p]; rewrite ?muln0 ?div0n //.
rewrite {1}(divn_eq m (n.+1 * p.+1)) mulnA mulnAC !divn_addl_mul //.
by rewrite addnC divn_small // ltn_divl // mulnC ltn_mod.
Qed.
Lemma divnAC : forall m n p, m %/ n %/ p = m %/ p %/ n.
Proof. by move=> m n p; rewrite !divn_divl mulnC. Qed.
Lemma modn_small : forall m d, m < d -> m %% d = m.
Proof. by move=> m d lt_md; rewrite {2}(divn_eq m d) divn_small. Qed.
Lemma modn_mod : forall m d, m %% d = m %[mod d].
Proof. by move=> m [|d] //; apply: modn_small; rewrite ltn_mod. Qed.
Lemma modn_addl_mul : forall p m d, p * d + m = m %[mod d].
Proof.
move=> p m d; case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
by rewrite {1}(divn_eq m d) addnA -muln_addl modn_def edivn_eq // ltn_mod.
Qed.
Lemma modn_pmul2l : forall p m d, 0 < p -> p * m %% (p * d) = p * (m %% d).
Proof.
move=> p m d p_gt0; apply: (@addnI (p * (m %/ d * d))).
by rewrite -muln_addr -divn_eq mulnCA -(divn_pmul2l p_gt0) -divn_eq.
Qed.
Implicit Arguments modn_pmul2l [p m d].
Lemma modn_addl : forall m d, d + m = m %[mod d].
Proof. by move=> m d; rewrite -{1}[d]mul1n modn_addl_mul. Qed.
Lemma modn_addr : forall m d, m + d = m %[mod d].
Proof. by move=> *; rewrite addnC modn_addl. Qed.
Lemma modnn : forall d, d %% d = 0.
Proof. by move=> d; rewrite -{1}[d]addn0 modn_addl mod0n. Qed.
Lemma modn_mull : forall p d, p * d %% d = 0.
Proof. by move=> p d; rewrite -[p * d]addn0 modn_addl_mul mod0n. Qed.
Lemma modn_mulr : forall p d, d * p %% d = 0.
Proof. by move=> p d; rewrite mulnC modn_mull. Qed.
Lemma modn_addml : forall m n d, m %% d + n = m + n %[mod d].
Proof. by move=> m n d; rewrite {2}(divn_eq m d) -addnA modn_addl_mul. Qed.
Lemma modn_addmr : forall m n d, m + n %% d = m + n %[mod d].
Proof. by move=> m n d; rewrite !(addnC m) modn_addml. Qed.
Lemma modn_add2m : forall m n d, m %% d + n %% d = m + n %[mod d].
Proof. by move=> m n d; rewrite modn_addml modn_addmr. Qed.
Lemma modn_mulml : forall m n d, m %% d * n = m * n %[mod d].
Proof.
by move=> m n d; rewrite {2}(divn_eq m d) muln_addl mulnAC modn_addl_mul.
Qed.
Lemma modn_mulmr : forall m n d, m * (n %% d) = m * n %[mod d].
Proof. by move=> m n d; rewrite !(mulnC m) modn_mulml. Qed.
Lemma modn_mul2m : forall m n d, m %% d * (n %% d) = m * n %[mod d].
Proof. by move=> m n d; rewrite modn_mulml modn_mulmr. Qed.
Lemma modn2 : forall m, m %% 2 = odd m.
Proof. by elim=> //= m IHm; rewrite -addn1 -modn_addml IHm; case odd. Qed.
Lemma divn2 : forall m, m %/ 2 = m./2.
Proof.
by move=> m; rewrite {2}(divn_eq m 2) modn2 muln2 addnC half_bit_double.
Qed.
Lemma odd_mod : forall m d, odd d = false -> odd (m %% d) = odd m.
Proof.
by move=> m d d_even; rewrite {2}(divn_eq m d) odd_add odd_mul d_even andbF.
Qed.
Lemma modn_exp: forall m n a, (a %% n) ^ m = a ^ m %[mod n].
Proof.
by elim=> // m Hrec n a; rewrite !expnS -modn_mulmr Hrec modn_mulml modn_mulmr.
Qed.
Divisibility
Definition dvdn d m := m %% d == 0.
Notation "m %| d" := (dvdn m d) (at level 70, no associativity) : nat_scope.
Lemma dvdn2 : forall n, (2 %| n) = ~~ odd n.
Proof. by move=> n; rewrite /dvdn modn2; case (odd n). Qed.
Lemma dvdnP : forall d m, reflect (exists k, m = k * d) (d %| m).
Proof.
move=> d m; apply: (iffP eqP) => [Hm | [k ->]]; last by rewrite modn_mull.
by exists (m %/ d); rewrite {1}(divn_eq m d) Hm addn0.
Qed.
Implicit Arguments dvdnP [d m].
Prenex Implicits dvdnP.
Lemma dvdn0 : forall d, d %| 0.
Proof. by case. Qed.
Lemma dvd0n : forall n, (0 %| n) = (n == 0).
Proof. by case. Qed.
Lemma dvdn1 : forall d, (d %| 1) = (d == 1).
Proof. by case=> [|[|n]] //; rewrite /dvdn modn_small. Qed.
Lemma dvd1n : forall m, 1 %| m.
Proof. by move=> m; rewrite /dvdn modn1. Qed.
Lemma dvdn_gt0 : forall d m, m > 0 -> d %| m -> d > 0.
Proof. by do 2!case. Qed.
Lemma dvdnn: forall m, m %| m.
Proof. by move=> m; rewrite /dvdn modnn. Qed.
Lemma dvdn_mull: forall d m n, d %| n -> d %| m * n.
Proof. by move=> d m n; case/dvdnP=> n' ->; rewrite /dvdn mulnA modn_mull. Qed.
Lemma dvdn_mulr: forall d m n, d %| m -> d %| m * n.
Proof. by move=> d m n d_m; rewrite mulnC dvdn_mull. Qed.
Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr.
Lemma dvdn_mul: forall d1 d2 m1 m2, d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
Proof.
move=> d1 d2 m1 m2; case/dvdnP=> q1 ->; case/dvdnP=> q2 ->.
by rewrite mulnCA -mulnA 2?dvdn_mull.
Qed.
Lemma dvdn_trans: forall n d m, d %| n -> n %| m -> d %| m.
Proof. move=> n d m Hn; move/dvdnP => [n1 ->]; exact: dvdn_mull. Qed.
Lemma dvdn_eq : forall d m, (d %| m) = (m %/ d * d == m).
Proof.
move=> d m; apply/eqP/eqP=> [modm0 | <-]; last exact: modn_mull.
by rewrite {2}(divn_eq m d) modm0 addn0.
Qed.
Lemma divnK : forall d m, d %| m -> m %/ d * d = m.
Proof. by move=> m d; rewrite dvdn_eq; move/eqP. Qed.
Lemma leq_divl : forall d m n, d %| m -> (m %/ d <= n) = (m <= n * d).
Proof. by case=> [[]//|d] m n dv_d_m; rewrite -(@leq_pmul2r d.+1) ?divnK. Qed.
Lemma ltn_divr : forall d m n, d %| m -> (n < m %/ d) = (n * d < m).
Proof. by move=> d m n dv_d_m; rewrite !ltnNge leq_divl. Qed.
Lemma eqn_div : forall d m n, d > 0 -> d %| m -> (n == m %/ d) = (n * d == m).
Proof. by move=> d m n d_gt0 dv_d_m; rewrite -(eqn_pmul2r d_gt0) divnK. Qed.
Lemma eqn_mul : forall d m n, d > 0 -> d %| m -> (m == n * d) = (m %/ d == n).
Proof. by move=> d m n d_gt0 dv_d_m; rewrite eq_sym -eqn_div // eq_sym. Qed.
Lemma divn_mulAC : forall d m n, d %| m -> m %/ d * n = m * n %/ d.
Proof.
case=> [[]//|d] m n dv_d_m; apply/eqP.
by rewrite eqn_div ?dvdn_mulr // mulnAC divnK.
Qed.
Lemma divn_mulA : forall d m n, d %| n -> m * (n %/ d) = m * n %/ d.
Proof. by move=> d m n dv_d_m; rewrite !(mulnC m) divn_mulAC. Qed.
Lemma divn_mulCA : forall d m n,
d %| m -> d %| n -> m * (n %/ d) = n * (m %/ d).
Proof. by move=> d m n dv_d_m dv_d_n; rewrite mulnC divn_mulAC ?divn_mulA. Qed.
Lemma divn_divr : forall m n p, p %| n -> m %/ (n %/ p) = m * p %/ n.
Proof. by move=> m n [|p] dv_n; rewrite -{2}(divnK dv_n) // divn_pmul2r. Qed.
Lemma modn_dvdm : forall m n d, d %| m -> n %% m = n %[mod d].
Proof.
move=> m n d; case/dvdnP=> q def_m.
by rewrite {2}(divn_eq n m) {3}def_m mulnA modn_addl_mul.
Qed.
Lemma dvdn_leq : forall d m, 0 < m -> d %| m -> d <= m.
Proof.
by move=> d m m_gt0; case/dvdnP=> [[|k] Dm]; rewrite Dm // leq_addr in m_gt0 *.
Qed.
Lemma gtnNdvd : forall n d, 0 < n -> n < d -> (d %| n) = false.
Proof. by move=> n d n_gt0 ltnd; rewrite /dvdn eqn0Ngt modn_small ?n_gt0. Qed.
Lemma eqn_dvd : forall m n, (m == n) = (m %| n) && (n %| m).
Proof.
case=> [|m] [|n] //; apply/idP/andP; first by move/eqP->; auto.
rewrite eqn_leq => [[Hmn Hnm]]; apply/andP; have:= dvdn_leq; auto.
Qed.
Lemma dvdn_pmul2l : forall p d m, 0 < p -> (p * d %| p * m) = (d %| m).
Proof. by case=> // p d m _; rewrite /dvdn modn_pmul2l // muln_eq0. Qed.
Implicit Arguments dvdn_pmul2l [p m d].
Lemma dvdn_pmul2r : forall p d m, 0 < p -> (d * p %| m * p) = (d %| m).
Proof. by move=> n d m Hn; rewrite -!(mulnC n) dvdn_pmul2l. Qed.
Implicit Arguments dvdn_pmul2r [p m d].
Lemma dvdn_addr : forall m d n, d %| m -> (d %| m + n) = (d %| n).
Proof. by move=> n d m; move/dvdnP=> [k ->]; rewrite /dvdn modn_addl_mul. Qed.
Lemma dvdn_addl : forall n d m, d %| n -> (d %| m + n) = (d %| m).
Proof. by move=> n d m; rewrite addnC; exact: dvdn_addr. Qed.
Lemma dvdn_add : forall d m n, d %| m -> d %| n -> d %| m + n.
Proof. by move=> n d m; move/dvdn_addr->. Qed.
Lemma dvdn_add_eq : forall d m n, d %| m + n -> (d %| m) = (d %| n).
Proof. by move=> *; apply/idP/idP; [move/dvdn_addr <-| move/dvdn_addl <-]. Qed.
Lemma dvdn_subr : forall d m n, n <= m -> d %| m -> (d %| m - n) = (d %| n).
Proof. by move=> d m n le_n_m dv_d_m; apply: dvdn_add_eq; rewrite subnK. Qed.
Lemma dvdn_subl : forall d m n, n <= m -> d %| n -> (d %| m - n) = (d %| m).
Proof. by move=> d m n le_n_m dv_d_m; rewrite -(dvdn_addl _ dv_d_m) subnK. Qed.
Lemma dvdn_sub : forall d m n, d %|m -> d %| n -> d %| m - n.
Proof.
move=> d n m; case: (leqP m n) => Hm; first by move/dvdn_subr <-.
by rewrite (eqnP (ltnW Hm)) dvdn0.
Qed.
Lemma dvdn_exp : forall k d m, 0 < k -> d %| m -> d %| (m ^ k).
Proof. by case=> // *; rewrite expnS dvdn_mulr. Qed.
Hint Resolve dvdn_add dvdn_sub dvdn_exp.
Lemma eqn_mod_dvd : forall d m n, n <= m -> (m == n %[mod d]) = (d %| m - n).
Proof.
rewrite /dvdn => d m n le_nm; apply/eqP/eqP => [eq_mod | mod_mn_0]; last first.
by rewrite -(subnK le_nm) -modn_addml mod_mn_0.
by rewrite (divn_eq m d) (divn_eq n d) eq_mod subn_add2r -muln_subl modn_mull.
Qed.
Lemma divn_addl : forall m n d, d %| m -> (m + n) %/ d = m %/ d + n %/ d.
Proof. by move=> m n [//|d] dv_m; rewrite -{1}(divnK dv_m) divn_addl_mul. Qed.
Lemma divn_addr : forall m n d, d %| n -> (m + n) %/ d = m %/ d + n %/ d.
Proof. by move=> m n d dv_n; rewrite addnC divn_addl // addnC. Qed.
Fixpoint gcdn_rec (m n : nat) {struct m} :=
let n' := n %% m in if n' is 0 then m else
if m - n'.-1 is m'.+1 then gcdn_rec (m' %% n') n' else n'.
Definition gcdn := nosimpl gcdn_rec.
Lemma gcdnE : forall m n, gcdn m n = if m == 0 then n else gcdn (n %% m) m.
Proof.
rewrite /gcdn => m; elim: m {-2}m (leqnn m) => [|s IHs] [|m] le_ms [|n] //=.
case def_n': (_ %% _) => // [n'].
have{def_n'} lt_n'm: n' < m by rewrite -def_n' -ltnS ltn_pmod.
rewrite {}IHs ?(leq_trans lt_n'm) // subn_if_gt ltnW //=; congr gcdn_rec.
by rewrite -{2}(subnK (ltnW lt_n'm)) -addnS modn_addr.
Qed.
Lemma gcdnn : idempotent gcdn.
Proof. by case=> // n; rewrite gcdnE modnn. Qed.
Lemma gcdnC : commutative gcdn.
Proof.
move=> m n; wlog lt_nm: m n / n < m.
by case: (ltngtP n m) => [||->]; [|symmetry|rewrite gcdnn]; auto.
by rewrite gcdnE -{1}(ltn_predK lt_nm) modn_small.
Qed.
Lemma gcd0n : left_id 0 gcdn. Proof. by case. Qed.
Lemma gcdn0 : right_id 0 gcdn. Proof. by case. Qed.
Lemma gcd1n : left_zero 1 gcdn.
Proof. by move=> n; rewrite gcdnE modn1. Qed.
Lemma gcdn1 : right_zero 1 gcdn.
Proof. by move=> n; rewrite gcdnC gcd1n. Qed.
Lemma dvdn_gcdr : forall m n, gcdn m n %| n.
Proof.
move=> m; elim: m {-2}m (leqnn m) => [|s IHs] [|m] le_ms [|n] //.
rewrite gcdnE; case def_n': (_ %% _) => [|n']; first by rewrite /dvdn def_n'.
have lt_n's: n' < s by rewrite -ltnS (leq_trans _ le_ms) // -def_n' ltn_pmod.
rewrite /= (divn_eq n.+1 m.+1) def_n' dvdn_addr ?dvdn_mull //; last exact: IHs.
by rewrite gcdnE /= IHs // (leq_trans _ lt_n's) // ltnW // ltn_pmod.
Qed.
Lemma dvdn_gcdl : forall m n, gcdn m n %| m.
Proof. by move=> m n; rewrite gcdnC dvdn_gcdr. Qed.
Lemma gcdn_gt0 : forall m n, (0 < gcdn m n) = (0 < m) || (0 < n).
Proof.
move=> [|m] [|n] //; apply: (@dvdn_gt0 _ m.+1) => //; exact: dvdn_gcdl.
Qed.
Lemma gcdn_addl_mul : forall k m n, gcdn m (k * m + n) = gcdn m n.
Proof. by move=> k m n; rewrite !(gcdnE m) modn_addl_mul mulnC; case: m. Qed.
Lemma gcdn_addl: forall m n, gcdn m (m + n) = gcdn m n.
Proof. by move => m n; rewrite -{2}(mul1n m) gcdn_addl_mul. Qed.
Lemma gcdn_addr: forall m n, gcdn m (n + m) = gcdn m n.
Proof. by move=> m n; rewrite addnC gcdn_addl. Qed.
Lemma gcdn_mull : forall n m, gcdn n (m * n) = n.
Proof. by move=> n m; rewrite gcdnE modn_mull gcd0n; case defn:n=> /=. Qed.
Lemma gcdn_mulr : forall n m, gcdn n (n * m) = n.
Proof. by move=> n m; rewrite mulnC gcdn_mull. Qed.
Fixpoint bezout_rec (km kn : nat) (qs : seq nat) {struct qs} :=
if qs is q :: qs' then bezout_rec kn (NatTrec.add_mul q kn km) qs'
else (km, kn).
Fixpoint egcdn_rec (m n s : nat) (qs : seq nat) {struct s} :=
if s is s'.+1 then
let: (q, r) := edivn m n in
if r > 0 then egcdn_rec n r s' (q :: qs) else
if odd (size qs) then qs else q.-1 :: qs
else [::0].
Definition egcdn m n := bezout_rec 0 1 (egcdn_rec m n n [::]).
CoInductive egcdn_spec (m n : nat) : nat * nat -> Type :=
EgcdnSpec km kn of km * m = kn * n + gcdn m n & kn * gcdn m n < m :
egcdn_spec m n (km, kn).
Lemma egcd0n : forall n, egcdn 0 n = (1, 0).
Proof. by case. Qed.
Lemma egcdnP : forall m n, m > 0 -> egcdn_spec m n (egcdn m n).
Proof.
rewrite /egcdn => m0 n0; have: (n0, m0) = bezout_rec n0 m0 [::] by [].
case: (posnP n0) => [-> /=|]; first by split; rewrite // mul1n gcdn0.
elim: {1 4}n0 {1 3 5 7}n0 {-1 4}m0 [::] (ltnSn n0) => [[]//|s IHs] n m qs /=.
move=> le_ns n_gt0 def_mn0 m_gt0.
case: edivnP => q r def_m; rewrite n_gt0 /= => lt_rn.
case: posnP => [r0 {s le_ns IHs lt_rn}|r_gt0]; last first.
by apply: IHs => //=; [rewrite (leq_trans lt_rn) | rewrite natTrecE -def_m].
rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n.
pose km := ~~ b : nat; pose kn := if b then 1 else q.-1.
rewrite (_ : bezout_rec _ _ _ = bezout_rec km kn qs); last first.
by rewrite /kn /km; case b => //=; rewrite natTrecE addn0 muln1.
have def_d: d = n by rewrite /d def_m gcdnC gcdnE modn_mull gcd0n -[n]prednK.
have: km * m + 2 * b * d = kn * n + d.
rewrite {}/kn {}/km def_m def_d -mulSnr; case: b; rewrite //= addn0 mul1n.
by rewrite prednK //; apply: dvdn_gt0 m_gt0 _; rewrite def_m dvdn_mulr.
have{def_m}: kn * d <= m.
have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0.
by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred.
have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1.
move: km {q}kn m_gt0 n_gt0 def_mn0; rewrite {}/d {}/b.
elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=.
case=> -> -> {m0 n0}; rewrite !addn0 => le_kn_r _ def_d; split=> //.
have d_gt0: 0 < gcdn n r by rewrite gcdn_gt0 n_gt0.
have: 0 < kn * n by rewrite def_d addn_gt0 d_gt0 orbT.
rewrite muln_gt0 n_gt0 andbT; move/ltn_pmul2l <-.
by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT.
rewrite !natTrecE; set m:= _ + r; set km := _ * _ + kn; pose d := gcdn m n.
have ->: gcdn n r = d by rewrite [d]gcdnC gcdn_addl_mul.
have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
move/IHq=> {IHq} IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
by rewrite muln_addl leq_add // -mulnA leq_mul2l le_kr_n orbT.
apply: (@addIn d); rewrite -!addnA addnn addnCA muln_addr -addnA addnCA.
rewrite /km muln_addl mulnCA mulnA -addnA; congr (_ + _).
by rewrite -def_d addnC -addnA -muln_addl -muln_addr addn_negb -mul2n.
Qed.
Lemma bezoutl : forall m n, m > 0 -> {a | a < m & m %| gcdn m n + a * n}.
Proof.
move=> m n m_gt0; case: (egcdnP n m_gt0) => km kn def_d lt_kn_m.
exists kn; last by rewrite addnC -def_d dvdn_mull.
apply: leq_ltn_trans lt_kn_m.
by rewrite -{1}[kn]muln1 leq_mul2l gcdn_gt0 m_gt0 orbT.
Qed.
Lemma bezoutr : forall m n, n > 0 -> {a | a < n & n %| gcdn m n + a * m}.
Proof. by move=> m n; rewrite gcdnC; exact: bezoutl. Qed.
Lemma dvdn_gcd : forall p m n, p %| gcdn m n = (p %| m) && (p %| n).
Proof.
move=> p m n; apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]].
by rewrite ?(dvdn_trans dv_pmn) ?dvdn_gcdl ?dvdn_gcdr.
case (posnP n) => [->|n_gt0]; first by rewrite gcdn0.
case: (bezoutr m n_gt0) => // km _; move/(dvdn_trans dv_pn).
by rewrite dvdn_addl // dvdn_mull.
Qed.
Lemma gcdn_mul2l : forall p m n, gcdn (p * m) (p * n) = p * gcdn m n.
Proof.
move=> p m n; case: (posnP p) => [-> //| p_gt0].
elim: {m}m.+1 {-2}m n (ltnSn m) => // s IHs m n; rewrite ltnS => le_ms.
rewrite gcdnE (gcdnE m) muln_eq0 modn_pmul2l // eqn0Ngt p_gt0.
case: posnP => // m_gt0; apply: IHs; apply: leq_trans le_ms.
exact: ltn_pmod.
Qed.
Lemma gcdn_modr : forall m n, gcdn m (n %% m) = gcdn m n.
Proof. by move=> m n; rewrite {2}(divn_eq n m) gcdn_addl_mul. Qed.
Lemma gcdn_modl: forall m n, gcdn (m %% n) n = gcdn m n.
Proof. by move=> m n; rewrite !(gcdnC _ n) gcdn_modr. Qed.
Lemma gcdnAC : right_commutative gcdn.
Proof.
suff dvd: forall m n p, gcdn (gcdn m n) p %| gcdn (gcdn m p) n.
by move=> m n p; apply/eqP; rewrite eqn_dvd !dvd.
move=> m n p; rewrite !dvdn_gcd dvdn_gcdr.
by rewrite !(dvdn_trans (dvdn_gcdl _ p)) ?dvdn_gcdl ?dvdn_gcdr.
Qed.
Lemma gcdnA : associative gcdn.
Proof. by move=> m n p; rewrite !(gcdnC m) gcdnAC. Qed.
Lemma gcdnCA : left_commutative gcdn.
Proof. by move=> m n p; rewrite !gcdnA (gcdnC m). Qed.
Lemma muln_gcdl : left_distributive muln gcdn.
Proof. by move=> m n p; rewrite -!(mulnC p) gcdn_mul2l. Qed.
Lemma muln_gcdr : right_distributive muln gcdn.
Proof. by move=> m n p; rewrite gcdn_mul2l. Qed.
Lemma gcdn_def : forall d m n,
d %| m -> d %| n -> (forall d', d' %| m -> d' %| n -> d' %| d)
-> gcdn m n = d.
Proof.
move=> d m n dv_dm dv_dn gdv_d; apply/eqP.
by rewrite eqn_dvd dvdn_gcd dv_dm dv_dn gdv_d ?dvdn_gcdl ?dvdn_gcdr.
Qed.
Lemma gcdn_divnC : forall n m, n * (m %/ gcdn n m) = m * (n %/ gcdn n m).
Proof. by move=> n m; rewrite divn_mulCA ?dvdn_gcdl ?dvdn_gcdr. Qed.
Definition lcmn m n := m * n %/ gcdn m n.
Lemma lcmnC : commutative lcmn.
Proof. by move=> m n; rewrite /lcmn mulnC gcdnC. Qed.
Lemma lcm0n : left_zero 0 lcmn. Proof. move=> n; exact: div0n. Qed.
Lemma lcmn0 : right_zero 0 lcmn. Proof. by move=> n; rewrite lcmnC lcm0n. Qed.
Lemma lcm1n : left_id 1 lcmn.
Proof. by move=> n; rewrite /lcmn gcd1n mul1n divn1. Qed.
Lemma lcmn1 : right_id 1 lcmn.
Proof. by move=> n; rewrite lcmnC lcm1n. Qed.
Lemma muln_lcm_gcd : forall m n, lcmn m n * gcdn m n = m * n.
Proof. by move=> m n; apply/eqP; rewrite divnK ?dvdn_mull ?dvdn_gcdr. Qed.
Lemma lcmn_gt0 : forall m n, (0 < lcmn m n) = (0 < m) && (0 < n).
Proof. by move=> m n; rewrite -muln_gt0 ltn_divr ?dvdn_mull ?dvdn_gcdr. Qed.
Lemma muln_lcmr : right_distributive muln lcmn.
Proof.
case=> // m n p; rewrite /lcmn -muln_gcdr -!mulnA divn_pmul2l // mulnCA.
by rewrite divn_mulA ?dvdn_mull ?dvdn_gcdr.
Qed.
Lemma muln_lcml : left_distributive muln lcmn.
Proof. by move=> m n p; rewrite -!(mulnC p) muln_lcmr. Qed.
Lemma lcmnA : associative lcmn.
Proof.
move=> m n p; rewrite {1 3}/lcmn mulnC !divn_mulAC ?dvdn_mull ?dvdn_gcdr //.
rewrite !divn_divl ?dvdn_mulr ?dvdn_gcdl // mulnC mulnA !muln_gcdr.
by rewrite ![_ * lcmn _ _]mulnC !muln_lcm_gcd !muln_gcdl -!(mulnC m) gcdnA.
Qed.
Lemma dvdn_lcml : forall d1 d2, d1 %| lcmn d1 d2.
Proof. by move=> d1 d2; rewrite /lcmn -divn_mulA ?dvdn_gcdr ?dvdn_mulr. Qed.
Lemma dvdn_lcmr : forall d1 d2, d2 %| lcmn d1 d2.
Proof. by move=> d1 d2; rewrite lcmnC dvdn_lcml. Qed.
Lemma dvdn_lcm : forall d1 d2 m, lcmn d1 d2 %| m = (d1 %| m) && (d2 %| m).
Proof.
case=> [|d1] [|d2] m; try by case: m => [|m]; rewrite ?lcmn0 ?andbF.
rewrite -(@dvdn_pmul2r (gcdn d1.+1 d2.+1)) ?gcdn_gt0 // muln_lcm_gcd.
by rewrite muln_gcdr dvdn_gcd {1}mulnC andbC !dvdn_pmul2r.
Qed.
Definition coprime m n := gcdn m n == 1.
Lemma coprime1n : forall n, coprime 1 n.
Proof. by move=> n; rewrite /coprime gcd1n. Qed.
Lemma coprimen1 : forall n, coprime n 1.
Proof. by move=> n; rewrite /coprime gcdn1. Qed.
Lemma coprime_sym : forall m n, coprime m n = coprime n m.
Proof. by move => m n; rewrite /coprime gcdnC. Qed.
Lemma coprime_modl : forall m n, coprime (m %% n) n = coprime m n.
Proof. by move=> m n; rewrite /coprime gcdn_modl. Qed.
Lemma coprime_modr : forall m n, coprime m (n %% m) = coprime m n.
Proof. by move=> m n; rewrite /coprime gcdn_modr. Qed.
Lemma coprimeP : forall n m, n > 0 ->
reflect (exists u, u.1 * n - u.2 * m = 1) (coprime n m).
Proof.
move=> n m n_gt0; apply: (iffP eqP) => [<-| [[kn km] /= kn_km_1]].
by have [kn km kg _] := egcdnP m n_gt0; exists (kn, km); rewrite kg addKn.
apply gcdn_def; rewrite ?dvd1n // => d dv_d_n dv_d_m.
by rewrite -kn_km_1 dvdn_subr ?dvdn_mull // ltnW // -subn_gt0 kn_km_1.
Qed.
Lemma modn_coprime : forall k n, O < k ->
(exists u, (k * u) %% n = 1%N) -> coprime k n.
Proof.
move=> k n Hpos [u Hu]; apply/coprimeP; first by [].
by exists (u, k * u %/ n); rewrite /= mulnC {1}(divn_eq (k * u) n) addKn.
Qed.
Lemma gauss_inv : forall m n p,
coprime m n -> (m * n %| p) = (m %| p) && (n %| p).
Proof.
by move=> m n p co_mn; rewrite -muln_lcm_gcd (eqnP co_mn) muln1 dvdn_lcm.
Qed.
Lemma gauss : forall m n p, coprime m n -> (m %| n * p) = (m %| p).
Proof.
move=> m [|n] p co_mn; first by case: m co_mn => [|[]] // _; rewrite !dvd1n.
by symmetry; rewrite mulnC -(@dvdn_pmul2r n.+1) ?gauss_inv // andbC dvdn_mull.
Qed.
Lemma gauss_gcdr : forall p m n, coprime p m -> gcdn p (m * n) = gcdn p n.
Proof.
move=> p m n co_pm; apply/eqP; rewrite eqn_dvd !dvdn_gcd !dvdn_gcdl /=.
rewrite andbC dvdn_mull ?dvdn_gcdr //= -(@gauss _ m) ?dvdn_gcdr //.
by rewrite /coprime gcdnAC (eqnP co_pm) gcd1n.
Qed.
Lemma gauss_gcdl : forall p m n, coprime p n -> gcdn p (m * n) = gcdn p m.
Proof. by move=> *; rewrite mulnC gauss_gcdr. Qed.
Lemma coprime_mulr : forall p m n,
coprime p (m * n) = coprime p m && coprime p n.
Proof.
move=> p m n.
case co_pm: (coprime p m) => /=; first by rewrite /coprime gauss_gcdr.
apply/eqP=> co_p_mn; case/eqnP: co_pm; apply gcdn_def => // d dv_dp dv_dm.
by rewrite -co_p_mn dvdn_gcd dv_dp dvdn_mulr.
Qed.
Lemma coprime_mull : forall p m n,
coprime (m * n) p = coprime m p && coprime n p.
Proof. move=> p m n; rewrite !(coprime_sym _ p); exact: coprime_mulr. Qed.
Lemma coprime_pexpl : forall k m n, 0 < k -> coprime (m ^ k) n = coprime m n.
Proof.
case=> // k m n _; elim: k => [|k IHk]; first by rewrite expn1.
by rewrite expnS coprime_mull -IHk; case coprime.
Qed.
Lemma coprime_pexpr : forall k m n, 0 < k -> coprime m (n ^ k) = coprime m n.
Proof. by move=> k m n k_gt0; rewrite !(coprime_sym m) coprime_pexpl. Qed.
Lemma coprime_expl : forall k m n, coprime m n -> coprime (m ^ k) n.
Proof. by case=> [|k] p m co_pm; rewrite ?coprime1n // coprime_pexpl. Qed.
Lemma coprime_expr : forall k m n, coprime m n -> coprime m (n ^ k).
Proof. by move=> k m n; rewrite !(coprime_sym m); exact: coprime_expl. Qed.
Lemma coprime_egcdn : forall n m, n > 0 ->
coprime (egcdn n m).1 (egcdn n m).2.
Proof.
move=> n m n_gt0; case: (egcdnP m n_gt0) => kn km /=; move/eqP.
have [u defn] := dvdnP (dvdn_gcdl n m); have [v defm] := dvdnP (dvdn_gcdr n m).
rewrite -[gcdn n m]mul1n {1}defm {1}defn !mulnA -muln_addl addnC.
rewrite eqn_pmul2r ?gcdn_gt0 ?n_gt0 //; move/eqP; case: kn => // kn def_knu _.
by apply/coprimeP=> //; exists (u, v); rewrite mulnC def_knu mulnC addnK.
Qed.
Section Chinese.
Variables m1 m2 : nat.
Hypothesis co_m12 : coprime m1 m2.
Lemma chinese_remainder : forall x y,
(x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
Proof.
move=> x y; wlog le_yx : x y / y <= x.
by case/orP: (leq_total y x); last rewrite !(eq_sym (x %% _)); auto.
by rewrite !eqn_mod_dvd // gauss_inv.
Qed.
Definition chinese r1 r2 :=
r1 * m2 * (egcdn m2 m1).1 + r2 * m1 * (egcdn m1 m2).1.
Lemma chinese_modl : forall r1 r2, chinese r1 r2 = r1 %[mod m1].
Proof.
rewrite /chinese; case: (posnP m2) co_m12 => [->|m2_gt0 _].
by move/eqnP; rewrite gcdn0 => -> r1 r2 ; rewrite !modn1.
case: egcdnP=> // k2 k1 def_m1 _ r1 r2.
rewrite mulnAC -mulnA def_m1 gcdnC (eqnP co_m12) muln_addr mulnA muln1.
by rewrite addnAC (mulnAC _ m1) -muln_addl modn_addl_mul.
Qed.
Lemma chinese_modr : forall r1 r2, chinese r1 r2 = r2 %[mod m2].
Proof.
rewrite /chinese; case: (posnP m1) co_m12 => [->|m1_gt0 _].
by move/eqnP; rewrite gcd0n => -> r1 r2 ; rewrite !modn1.
case: (egcdnP m2) => // k1 k2 def_m2 _ r1 r2.
rewrite addnC mulnAC -mulnA def_m2 (eqnP co_m12) muln_addr mulnA muln1.
by rewrite addnAC (mulnAC _ m2) -muln_addl modn_addl_mul.
Qed.
Lemma chinese_modlr : forall x, x = chinese (x %% m1) (x %% m2) %[mod m1 * m2].
Proof.
move=> x; apply/eqP.
by rewrite chinese_remainder // chinese_modl chinese_modr !modn_mod !eqxx.
Qed.
End Chinese.