From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.ssreflect.div.html | 451 +++++++++++++++---------------- 1 file changed, 225 insertions(+), 226 deletions(-) (limited to 'docs/htmldoc/mathcomp.ssreflect.div.html') diff --git a/docs/htmldoc/mathcomp.ssreflect.div.html b/docs/htmldoc/mathcomp.ssreflect.div.html index 1379bbb..0d39448 100644 --- a/docs/htmldoc/mathcomp.ssreflect.div.html +++ b/docs/htmldoc/mathcomp.ssreflect.div.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -62,26 +61,26 @@
Definition edivn_rec d :=
-  fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).
+  fix loop m q := 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).
+Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).

-CoInductive edivn_spec m d : nat × nat → Type :=
-  EdivnSpec q r of m = q × d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).
+Variant edivn_spec m d : nat × nat → Type :=
+  EdivnSpec q r of m = q × d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).

Lemma edivnP m d : edivn_spec m d (edivn m d).

-Lemma edivn_eq d q r : r < d → edivn (q × d + r) d = (q, r).
+Lemma edivn_eq d q r : r < d → edivn (q × d + r) d = (q, r).

-Definition divn m d := (edivn m d).1.
+Definition divn m d := (edivn m d).1.

-Notation "m %/ d" := (divn m d) : nat_scope.
+Notation "m %/ d" := (divn m d) : nat_scope.

@@ -92,176 +91,176 @@

-Definition modn_rec d := fix loop m := if m - d is m'.+1 then loop m' else m.
+Definition modn_rec d := fix loop m := 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.
+Definition modn m d := if d > 0 then modn_rec d.-1 m else m.

-Notation "m %% d" := (modn m d) : nat_scope.
-Notation "m = n %[mod d ]" := (m %% d = n %% d) : nat_scope.
-Notation "m == n %[mod d ]" := (m %% d == n %% d) : nat_scope.
-Notation "m <> n %[mod d ]" := (m %% d ≠ n %% d) : nat_scope.
-Notation "m != n %[mod d ]" := (m %% d != n %% d) : nat_scope.
+Notation "m %% d" := (modn m d) : nat_scope.
+Notation "m = n %[mod d ]" := (m %% d = n %% d) : nat_scope.
+Notation "m == n %[mod d ]" := (m %% d == n %% d) : nat_scope.
+Notation "m <> n %[mod d ]" := (m %% d ≠ n %% d) : nat_scope.
+Notation "m != n %[mod d ]" := (m %% d != n %% d) : nat_scope.

-Lemma modn_def m d : m %% d = (edivn m d).2.
+Lemma modn_def m d : m %% d = (edivn m d).2.

-Lemma edivn_def m d : edivn m d = (m %/ d, m %% d).
+Lemma edivn_def m d : edivn m d = (m %/ d, m %% d).

-Lemma divn_eq m d : m = m %/ d × d + m %% d.
+Lemma divn_eq m d : m = m %/ d × d + m %% d.

-Lemma div0n d : 0 %/ d = 0.
-Lemma divn0 m : m %/ 0 = 0.
-Lemma mod0n d : 0 %% d = 0.
-Lemma modn0 m : m %% 0 = m.
+Lemma div0n d : 0 %/ d = 0.
+Lemma divn0 m : m %/ 0 = 0.
+Lemma mod0n d : 0 %% d = 0.
+Lemma modn0 m : m %% 0 = m.

-Lemma divn_small m d : m < d → m %/ d = 0.
+Lemma divn_small m d : m < d → m %/ d = 0.

-Lemma divnMDl q m d : 0 < d → (q × d + m) %/ d = q + m %/ d.
+Lemma divnMDl q m d : 0 < d → (q × d + m) %/ d = q + m %/ d.

-Lemma mulnK m d : 0 < d → m × d %/ d = m.
+Lemma mulnK m d : 0 < d → m × d %/ d = m.

-Lemma mulKn m d : 0 < d → d × m %/ d = m.
+Lemma mulKn m d : 0 < d → d × m %/ d = m.

-Lemma expnB p m n : p > 0 → m ≥ n → p ^ (m - n) = p ^ m %/ p ^ n.
+Lemma expnB p m n : p > 0 → m ≥ n → p ^ (m - n) = p ^ m %/ p ^ n.

-Lemma modn1 m : m %% 1 = 0.
+Lemma modn1 m : m %% 1 = 0.

-Lemma divn1 m : m %/ 1 = m.
+Lemma divn1 m : m %/ 1 = m.

-Lemma divnn d : d %/ d = (0 < d).
+Lemma divnn d : d %/ d = (0 < d).

-Lemma divnMl p m d : p > 0 → p × m %/ (p × d) = m %/ d.
+Lemma divnMl p m d : p > 0 → p × m %/ (p × d) = m %/ d.

-Lemma divnMr p m d : p > 0 → m × p %/ (d × p) = m %/ d.
+Lemma divnMr p m d : p > 0 → m × p %/ (d × p) = m %/ d.

-Lemma ltn_mod m d : (m %% d < d) = (0 < d).
+Lemma ltn_mod m d : (m %% d < d) = (0 < d).

-Lemma ltn_pmod m d : 0 < d → m %% d < d.
+Lemma ltn_pmod m d : 0 < d → m %% d < d.

-Lemma leq_trunc_div m d : m %/ d × d ≤ m.
+Lemma leq_trunc_div m d : m %/ d × d ≤ m.

-Lemma leq_mod m d : m %% d ≤ m.
+Lemma leq_mod m d : m %% d ≤ m.

-Lemma leq_div m d : m %/ d ≤ m.
+Lemma leq_div m d : m %/ d ≤ m.

-Lemma ltn_ceil m d : 0 < d → m < (m %/ d).+1 × d.
+Lemma ltn_ceil m d : 0 < d → m < (m %/ d).+1 × d.

-Lemma ltn_divLR m n d : d > 0 → (m %/ d < n) = (m < n × d).
+Lemma ltn_divLR m n d : d > 0 → (m %/ d < n) = (m < n × d).

-Lemma leq_divRL m n d : d > 0 → (m ≤ n %/ d) = (m × d ≤ n).
+Lemma leq_divRL m n d : d > 0 → (m ≤ n %/ d) = (m × d ≤ n).

-Lemma ltn_Pdiv m d : 1 < d → 0 < m → m %/ d < m.
+Lemma ltn_Pdiv m d : 1 < d → 0 < m → m %/ d < m.

-Lemma divn_gt0 d m : 0 < d → (0 < m %/ d) = (d ≤ m).
+Lemma divn_gt0 d m : 0 < d → (0 < m %/ d) = (d ≤ m).

-Lemma leq_div2r d m n : m ≤ n → m %/ d ≤ n %/ d.
+Lemma leq_div2r d m n : m ≤ n → m %/ d ≤ n %/ d.

-Lemma leq_div2l m d e : 0 < d → d ≤ e → m %/ e ≤ m %/ d.
+Lemma leq_div2l m d e : 0 < d → d ≤ e → m %/ e ≤ m %/ d.

-Lemma leq_divDl p m n : (m + n) %/ p ≤ m %/ p + n %/ p + 1.
+Lemma leq_divDl p m n : (m + n) %/ p ≤ m %/ p + n %/ p + 1.

-Lemma geq_divBl k m p : k %/ p - m %/ p ≤ (k - m) %/ p + 1.
+Lemma geq_divBl k m p : k %/ p - m %/ p ≤ (k - m) %/ p + 1.

-Lemma divnMA m n p : m %/ (n × p) = m %/ n %/ p.
+Lemma divnMA m n p : m %/ (n × p) = m %/ n %/ p.

-Lemma divnAC m n p : m %/ n %/ p = m %/ p %/ n.
+Lemma divnAC m n p : m %/ n %/ p = m %/ p %/ n.

-Lemma modn_small m d : m < d → m %% d = m.
+Lemma modn_small m d : m < d → m %% d = m.

-Lemma modn_mod m d : m %% d = m %[mod d].
+Lemma modn_mod m d : m %% d = m %[mod d].

-Lemma modnMDl p m d : p × d + m = m %[mod d].
+Lemma modnMDl p m d : p × d + m = m %[mod d].

-Lemma muln_modr {p m d} : 0 < p → p × (m %% d) = (p × m) %% (p × d).
+Lemma muln_modr {p m d} : 0 < p → p × (m %% d) = (p × m) %% (p × d).

-Lemma muln_modl {p m d} : 0 < p → (m %% d) × p = (m × p) %% (d × p).
+Lemma muln_modl {p m d} : 0 < p → (m %% d) × p = (m × p) %% (d × p).

-Lemma modnDl m d : d + m = m %[mod d].
+Lemma modnDl m d : d + m = m %[mod d].

-Lemma modnDr m d : m + d = m %[mod d].
+Lemma modnDr m d : m + d = m %[mod d].

-Lemma modnn d : d %% d = 0.
+Lemma modnn d : d %% d = 0.

-Lemma modnMl p d : p × d %% d = 0.
+Lemma modnMl p d : p × d %% d = 0.

-Lemma modnMr p d : d × p %% d = 0.
+Lemma modnMr p d : d × p %% d = 0.

-Lemma modnDml m n d : m %% d + n = m + n %[mod d].
+Lemma modnDml m n d : m %% d + n = m + n %[mod d].

-Lemma modnDmr m n d : m + n %% d = m + n %[mod d].
+Lemma modnDmr m n d : m + n %% d = m + n %[mod d].

-Lemma modnDm m n d : m %% d + n %% d = m + n %[mod d].
+Lemma modnDm m n d : m %% d + n %% d = m + n %[mod d].

-Lemma eqn_modDl p m n d : (p + m == p + n %[mod d]) = (m == n %[mod d]).
+Lemma eqn_modDl p m n d : (p + m == p + n %[mod d]) = (m == n %[mod d]).

-Lemma eqn_modDr p m n d : (m + p == n + p %[mod d]) = (m == n %[mod d]).
+Lemma eqn_modDr p m n d : (m + p == n + p %[mod d]) = (m == n %[mod d]).

-Lemma modnMml m n d : m %% d × n = m × n %[mod d].
+Lemma modnMml m n d : m %% d × n = m × n %[mod d].

-Lemma modnMmr m n d : m × (n %% d) = m × n %[mod d].
+Lemma modnMmr m n d : m × (n %% d) = m × n %[mod d].

-Lemma modnMm m n d : m %% d × (n %% d) = m × n %[mod d].
+Lemma modnMm m n d : m %% d × (n %% d) = m × n %[mod d].

-Lemma modn2 m : m %% 2 = odd m.
+Lemma modn2 m : m %% 2 = odd m.

-Lemma divn2 m : m %/ 2 = m./2.
+Lemma divn2 m : m %/ 2 = m./2.

-Lemma odd_mod m d : odd d = false → odd (m %% d) = odd m.
+Lemma odd_mod m d : odd d = false → odd (m %% d) = odd m.

-Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
+Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].

@@ -272,155 +271,155 @@

-Definition dvdn d m := m %% d == 0.
+Definition dvdn d m := m %% d == 0.

-Notation "m %| d" := (dvdn m d) : nat_scope.
+Notation "m %| d" := (dvdn m d) : nat_scope.

-Lemma dvdnP d m : reflect (∃ k, m = k × d) (d %| m).
+Lemma dvdnP d m : reflect (∃ k, m = k × d) (d %| m).

-Lemma dvdn0 d : d %| 0.
+Lemma dvdn0 d : d %| 0.

-Lemma dvd0n n : (0 %| n) = (n == 0).
+Lemma dvd0n n : (0 %| n) = (n == 0).

-Lemma dvdn1 d : (d %| 1) = (d == 1).
+Lemma dvdn1 d : (d %| 1) = (d == 1).

-Lemma dvd1n m : 1 %| m.
+Lemma dvd1n m : 1 %| m.

-Lemma dvdn_gt0 d m : m > 0 → d %| m → d > 0.
+Lemma dvdn_gt0 d m : m > 0 → d %| m → d > 0.

-Lemma dvdnn m : m %| m.
+Lemma dvdnn m : m %| m.

-Lemma dvdn_mull d m n : d %| n → d %| m × n.
+Lemma dvdn_mull d m n : d %| n → d %| m × n.

-Lemma dvdn_mulr d m n : d %| m → d %| m × n.
- Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr.
+Lemma dvdn_mulr d m n : d %| m → d %| m × n.
+ Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr : core.

-Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2.
+Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2.

-Lemma dvdn_trans n d m : d %| n → n %| m → d %| m.
+Lemma dvdn_trans n d m : d %| n → n %| m → d %| m.

-Lemma dvdn_eq d m : (d %| m) = (m %/ d × d == m).
+Lemma dvdn_eq d m : (d %| m) = (m %/ d × d == m).

-Lemma dvdn2 n : (2 %| n) = ~~ odd n.
+Lemma dvdn2 n : (2 %| n) = ~~ odd n.

-Lemma dvdn_odd m n : m %| n → odd n → odd m.
+Lemma dvdn_odd m n : m %| n → odd n → odd m.

-Lemma divnK d m : d %| m → m %/ d × d = m.
+Lemma divnK d m : d %| m → m %/ d × d = m.

-Lemma leq_divLR d m n : d %| m → (m %/ d ≤ n) = (m ≤ n × d).
+Lemma leq_divLR d m n : d %| m → (m %/ d ≤ n) = (m ≤ n × d).

-Lemma ltn_divRL d m n : d %| m → (n < m %/ d) = (n × d < m).
+Lemma ltn_divRL d m n : d %| m → (n < m %/ d) = (n × d < m).

-Lemma eqn_div d m n : d > 0 → d %| m → (n == m %/ d) = (n × d == m).
+Lemma eqn_div d m n : d > 0 → d %| m → (n == m %/ d) = (n × d == m).

-Lemma eqn_mul d m n : d > 0 → d %| m → (m == n × d) = (m %/ d == n).
+Lemma eqn_mul d m n : d > 0 → d %| m → (m == n × d) = (m %/ d == n).

-Lemma divn_mulAC d m n : d %| m → m %/ d × n = m × n %/ d.
+Lemma divn_mulAC d m n : d %| m → m %/ d × n = m × n %/ d.

-Lemma muln_divA d m n : d %| n → m × (n %/ d) = m × n %/ d.
+Lemma muln_divA d m n : d %| n → m × (n %/ d) = m × n %/ d.

-Lemma muln_divCA d m n : d %| m → d %| n → m × (n %/ d) = n × (m %/ d).
+Lemma muln_divCA d m n : d %| m → d %| n → m × (n %/ d) = n × (m %/ d).

-Lemma divnA m n p : p %| n → m %/ (n %/ p) = m × p %/ n.
+Lemma divnA m n p : p %| n → m %/ (n %/ p) = m × p %/ n.

-Lemma modn_dvdm m n d : d %| m → n %% m = n %[mod d].
+Lemma modn_dvdm m n d : d %| m → n %% m = n %[mod d].

-Lemma dvdn_leq d m : 0 < m → d %| m → d ≤ m.
+Lemma dvdn_leq d m : 0 < m → d %| m → d ≤ m.

-Lemma gtnNdvd n d : 0 < n → n < d → (d %| n) = false.
+Lemma gtnNdvd n d : 0 < n → n < d → (d %| n) = false.

-Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).
+Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).

-Lemma dvdn_pmul2l p d m : 0 < p → (p × d %| p × m) = (d %| m).
+Lemma dvdn_pmul2l p d m : 0 < p → (p × d %| p × m) = (d %| m).

-Lemma dvdn_pmul2r p d m : 0 < p → (d × p %| m × p) = (d %| m).
+Lemma dvdn_pmul2r p d m : 0 < p → (d × p %| m × p) = (d %| m).

-Lemma dvdn_divLR p d m : 0 < p → p %| d → (d %/ p %| m) = (d %| m × p).
+Lemma dvdn_divLR p d m : 0 < p → p %| d → (d %/ p %| m) = (d %| m × p).

-Lemma dvdn_divRL p d m : p %| m → (d %| m %/ p) = (d × p %| m).
+Lemma dvdn_divRL p d m : p %| m → (d %| m %/ p) = (d × p %| m).

-Lemma dvdn_div d m : d %| m → m %/ d %| m.
+Lemma dvdn_div d m : d %| m → m %/ d %| m.

-Lemma dvdn_exp2l p m n : m ≤ n → p ^ m %| p ^ n.
+Lemma dvdn_exp2l p m n : m ≤ n → p ^ m %| p ^ n.

-Lemma dvdn_Pexp2l p m n : p > 1 → (p ^ m %| p ^ n) = (m ≤ n).
+Lemma dvdn_Pexp2l p m n : p > 1 → (p ^ m %| p ^ n) = (m ≤ n).

-Lemma dvdn_exp2r m n k : m %| n → m ^ k %| n ^ k.
+Lemma dvdn_exp2r m n k : m %| n → m ^ k %| n ^ k.

-Lemma dvdn_addr m d n : d %| m → (d %| m + n) = (d %| n).
+Lemma dvdn_addr m d n : d %| m → (d %| m + n) = (d %| n).

-Lemma dvdn_addl n d m : d %| n → (d %| m + n) = (d %| m).
+Lemma dvdn_addl n d m : d %| n → (d %| m + n) = (d %| m).

-Lemma dvdn_add d m n : d %| m → d %| n → d %| m + n.
+Lemma dvdn_add d m n : d %| m → d %| n → d %| m + n.

-Lemma dvdn_add_eq d m n : d %| m + n → (d %| m) = (d %| n).
+Lemma dvdn_add_eq d m n : d %| m + n → (d %| m) = (d %| n).

-Lemma dvdn_subr d m n : n ≤ m → d %| m → (d %| m - n) = (d %| n).
+Lemma dvdn_subr d m n : n ≤ m → d %| m → (d %| m - n) = (d %| n).

-Lemma dvdn_subl d m n : n ≤ m → d %| n → (d %| m - n) = (d %| m).
+Lemma dvdn_subl d m n : n ≤ m → d %| n → (d %| m - n) = (d %| m).

-Lemma dvdn_sub d m n : d %| m → d %| n → d %| m - n.
+Lemma dvdn_sub d m n : d %| m → d %| n → d %| m - n.

-Lemma dvdn_exp k d m : 0 < k → d %| m → d %| (m ^ k).
+Lemma dvdn_exp k d m : 0 < k → d %| m → d %| (m ^ k).

-Lemma dvdn_fact m n : 0 < m ≤ n → m %| n`!.
+Lemma dvdn_fact m n : 0 < m ≤ n → m %| n`!.

-Hint Resolve dvdn_add dvdn_sub dvdn_exp.
+Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.

-Lemma eqn_mod_dvd d m n : n ≤ m → (m == n %[mod d]) = (d %| m - n).
+Lemma eqn_mod_dvd d m n : n ≤ m → (m == n %[mod d]) = (d %| m - n).

-Lemma divnDl m n d : d %| m → (m + n) %/ d = m %/ d + n %/ d.
+Lemma divnDl m n d : d %| m → (m + n) %/ d = m %/ d + n %/ d.

-Lemma divnDr m n d : d %| n → (m + n) %/ d = m %/ d + n %/ d.
+Lemma divnDr m n d : d %| n → (m + n) %/ d = m %/ d + n %/ d.

@@ -432,69 +431,69 @@
Fixpoint gcdn_rec m n :=
-  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'.
+  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.
+Definition gcdn := nosimpl gcdn_rec.

-Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m.
+Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m.

-Lemma gcdnn : idempotent gcdn.
+Lemma gcdnn : idempotent gcdn.

-Lemma gcdnC : commutative gcdn.
+Lemma gcdnC : commutative gcdn.

-Lemma gcd0n : left_id 0 gcdn.
-Lemma gcdn0 : right_id 0 gcdn.
+Lemma gcd0n : left_id 0 gcdn.
+Lemma gcdn0 : right_id 0 gcdn.

-Lemma gcd1n : left_zero 1 gcdn.
+Lemma gcd1n : left_zero 1 gcdn.

-Lemma gcdn1 : right_zero 1 gcdn.
+Lemma gcdn1 : right_zero 1 gcdn.

-Lemma dvdn_gcdr m n : gcdn m n %| n.
+Lemma dvdn_gcdr m n : gcdn m n %| n.

-Lemma dvdn_gcdl m n : gcdn m n %| m.
+Lemma dvdn_gcdl m n : gcdn m n %| m.

-Lemma gcdn_gt0 m n : (0 < gcdn m n) = (0 < m) || (0 < n).
+Lemma gcdn_gt0 m n : (0 < gcdn m n) = (0 < m) || (0 < n).

-Lemma gcdnMDl k m n : gcdn m (k × m + n) = gcdn m n.
+Lemma gcdnMDl k m n : gcdn m (k × m + n) = gcdn m n.

-Lemma gcdnDl m n : gcdn m (m + n) = gcdn m n.
+Lemma gcdnDl m n : gcdn m (m + n) = gcdn m n.

-Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n.
+Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n.

-Lemma gcdnMl n m : gcdn n (m × n) = n.
+Lemma gcdnMl n m : gcdn n (m × n) = n.

-Lemma gcdnMr n m : gcdn n (n × m) = n.
+Lemma gcdnMr n m : gcdn n (n × m) = n.

-Lemma gcdn_idPl {m n} : reflect (gcdn m n = m) (m %| n).
+Lemma gcdn_idPl {m n} : reflect (gcdn m n = m) (m %| n).

-Lemma gcdn_idPr {m n} : reflect (gcdn m n = n) (n %| m).
+Lemma gcdn_idPr {m n} : reflect (gcdn m n = n) (n %| m).

-Lemma expn_min e m n : e ^ minn m n = gcdn (e ^ m) (e ^ n).
+Lemma expn_min e m n : e ^ minn m n = gcdn (e ^ m) (e ^ n).

-Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.
+Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.

-Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n.
+Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n.

@@ -506,36 +505,36 @@
Fixpoint Bezout_rec km kn qs :=
-  if qs is q :: qs' then Bezout_rec kn (NatTrec.add_mul q kn km) qs'
-  else (km, kn).
+  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 qs :=
-  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].
+  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 [::]).
+Definition egcdn m n := Bezout_rec 0 1 (egcdn_rec m n n [::]).

-CoInductive egcdn_spec m n : 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).
+Variant egcdn_spec m n : 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 n : egcdn 0 n = (1, 0).
+Lemma egcd0n n : egcdn 0 n = (1, 0).

-Lemma egcdnP m n : m > 0 → egcdn_spec m n (egcdn m n).
+Lemma egcdnP m n : m > 0 → egcdn_spec m n (egcdn m n).

-Lemma Bezoutl m n : m > 0 → {a | a < m & m %| gcdn m n + a × n}.
+Lemma Bezoutl m n : m > 0 → {a | a < m & m %| gcdn m n + a × n}.

-Lemma Bezoutr m n : n > 0 → {a | a < n & n %| gcdn m n + a × m}.
+Lemma Bezoutr m n : n > 0 → {a | a < n & n %| gcdn m n + a × m}.

@@ -546,33 +545,33 @@

-Lemma dvdn_gcd p m n : p %| gcdn m n = (p %| m) && (p %| n).
+Lemma dvdn_gcd p m n : p %| gcdn m n = (p %| m) && (p %| n).

-Lemma gcdnAC : right_commutative gcdn.
+Lemma gcdnAC : right_commutative gcdn.

-Lemma gcdnA : associative gcdn.
+Lemma gcdnA : associative gcdn.

-Lemma gcdnCA : left_commutative gcdn.
+Lemma gcdnCA : left_commutative gcdn.

-Lemma gcdnACA : interchange gcdn gcdn.
+Lemma gcdnACA : interchange gcdn gcdn.

-Lemma muln_gcdr : right_distributive muln gcdn.
+Lemma muln_gcdr : right_distributive muln gcdn.

-Lemma muln_gcdl : left_distributive muln gcdn.
+Lemma muln_gcdl : left_distributive muln gcdn.

Lemma gcdn_def d m n :
-    d %| m → d %| n → (∀ d', d' %| m → d' %| n → d' %| d) →
-  gcdn m n = d.
+    d %| m → d %| n → (∀ d', d' %| m → d' %| n → d' %| d) →
+  gcdn m n = d.

-Lemma muln_divCA_gcd n m : n × (m %/ gcdn n m) = m × (n %/ gcdn n m).
+Lemma muln_divCA_gcd n m : n × (m %/ gcdn n m) = m × (n %/ gcdn n m).

@@ -583,68 +582,68 @@

-Definition lcmn m n := m × n %/ gcdn m n.
+Definition lcmn m n := m × n %/ gcdn m n.

-Lemma lcmnC : commutative lcmn.
+Lemma lcmnC : commutative lcmn.

-Lemma lcm0n : left_zero 0 lcmn.
-Lemma lcmn0 : right_zero 0 lcmn.
+Lemma lcm0n : left_zero 0 lcmn.
+Lemma lcmn0 : right_zero 0 lcmn.

-Lemma lcm1n : left_id 1 lcmn.
+Lemma lcm1n : left_id 1 lcmn.

-Lemma lcmn1 : right_id 1 lcmn.
+Lemma lcmn1 : right_id 1 lcmn.

-Lemma muln_lcm_gcd m n : lcmn m n × gcdn m n = m × n.
+Lemma muln_lcm_gcd m n : lcmn m n × gcdn m n = m × n.

-Lemma lcmn_gt0 m n : (0 < lcmn m n) = (0 < m) && (0 < n).
+Lemma lcmn_gt0 m n : (0 < lcmn m n) = (0 < m) && (0 < n).

-Lemma muln_lcmr : right_distributive muln lcmn.
+Lemma muln_lcmr : right_distributive muln lcmn.

-Lemma muln_lcml : left_distributive muln lcmn.
+Lemma muln_lcml : left_distributive muln lcmn.

-Lemma lcmnA : associative lcmn.
+Lemma lcmnA : associative lcmn.

-Lemma lcmnCA : left_commutative lcmn.
+Lemma lcmnCA : left_commutative lcmn.

-Lemma lcmnAC : right_commutative lcmn.
+Lemma lcmnAC : right_commutative lcmn.

-Lemma lcmnACA : interchange lcmn lcmn.
+Lemma lcmnACA : interchange lcmn lcmn.

-Lemma dvdn_lcml d1 d2 : d1 %| lcmn d1 d2.
+Lemma dvdn_lcml d1 d2 : d1 %| lcmn d1 d2.

-Lemma dvdn_lcmr d1 d2 : d2 %| lcmn d1 d2.
+Lemma dvdn_lcmr d1 d2 : d2 %| lcmn d1 d2.

-Lemma dvdn_lcm d1 d2 m : lcmn d1 d2 %| m = (d1 %| m) && (d2 %| m).
+Lemma dvdn_lcm d1 d2 m : lcmn d1 d2 %| m = (d1 %| m) && (d2 %| m).

-Lemma lcmnMl m n : lcmn m (m × n) = m × n.
+Lemma lcmnMl m n : lcmn m (m × n) = m × n.

-Lemma lcmnMr m n : lcmn n (m × n) = m × n.
+Lemma lcmnMr m n : lcmn n (m × n) = m × n.

-Lemma lcmn_idPr {m n} : reflect (lcmn m n = n) (m %| n).
+Lemma lcmn_idPr {m n} : reflect (lcmn m n = n) (m %| n).

-Lemma lcmn_idPl {m n} : reflect (lcmn m n = m) (n %| m).
+Lemma lcmn_idPl {m n} : reflect (lcmn m n = m) (n %| m).

-Lemma expn_max e m n : e ^ maxn m n = lcmn (e ^ m) (e ^ n).
+Lemma expn_max e m n : e ^ maxn m n = lcmn (e ^ m) (e ^ n).

@@ -655,7 +654,7 @@

-Definition coprime m n := gcdn m n == 1.
+Definition coprime m n := gcdn m n == 1.

Lemma coprime1n n : coprime 1 n.
@@ -664,89 +663,89 @@ Lemma coprimen1 n : coprime n 1.

-Lemma coprime_sym m n : coprime m n = coprime n m.
+Lemma coprime_sym m n : coprime m n = coprime n m.

-Lemma coprime_modl m n : coprime (m %% n) n = coprime m n.
+Lemma coprime_modl m n : coprime (m %% n) n = coprime m n.

-Lemma coprime_modr m n : coprime m (n %% m) = coprime m n.
+Lemma coprime_modr m n : coprime m (n %% m) = coprime m n.

-Lemma coprime2n n : coprime 2 n = odd n.
+Lemma coprime2n n : coprime 2 n = odd n.

-Lemma coprimen2 n : coprime n 2 = odd n.
+Lemma coprimen2 n : coprime n 2 = odd n.

-Lemma coprimeSn n : coprime n.+1 n.
+Lemma coprimeSn n : coprime n.+1 n.

-Lemma coprimenS n : coprime n n.+1.
+Lemma coprimenS n : coprime n n.+1.

-Lemma coprimePn n : n > 0 → coprime n.-1 n.
+Lemma coprimePn n : n > 0 → coprime n.-1 n.

-Lemma coprimenP n : n > 0 → coprime n n.-1.
+Lemma coprimenP n : n > 0 → coprime n n.-1.

Lemma coprimeP n m :
-  n > 0 → reflect (∃ u, u.1 × n - u.2 × m = 1) (coprime n m).
+  n > 0 → reflect (∃ u, u.1 × n - u.2 × m = 1) (coprime n m).

-Lemma modn_coprime k n : 0 < k → (∃ u, (k × u) %% n = 1) → coprime k n.
+Lemma modn_coprime k n : 0 < k → (∃ u, (k × u) %% n = 1) → coprime k n.

-Lemma Gauss_dvd m n p : coprime m n → (m × n %| p) = (m %| p) && (n %| p).
+Lemma Gauss_dvd m n p : coprime m n → (m × n %| p) = (m %| p) && (n %| p).

-Lemma Gauss_dvdr m n p : coprime m n → (m %| n × p) = (m %| p).
+Lemma Gauss_dvdr m n p : coprime m n → (m %| n × p) = (m %| p).

-Lemma Gauss_dvdl m n p : coprime m p → (m %| n × p) = (m %| n).
+Lemma Gauss_dvdl m n p : coprime m p → (m %| n × p) = (m %| n).

-Lemma dvdn_double_leq m n : m %| n → odd m → ~~ odd n → 0 < n → m.*2 ≤ n.
+Lemma dvdn_double_leq m n : m %| n → odd m → ~~ odd n → 0 < n → m.*2 ≤ n.

-Lemma dvdn_double_ltn m n : m %| n.-1 → odd m → odd n → 1 < n → m.*2 < n.
+Lemma dvdn_double_ltn m n : m %| n.-1 → odd m → odd n → 1 < n → m.*2 < n.

-Lemma Gauss_gcdr p m n : coprime p m → gcdn p (m × n) = gcdn p n.
+Lemma Gauss_gcdr p m n : coprime p m → gcdn p (m × n) = gcdn p n.

-Lemma Gauss_gcdl p m n : coprime p n → gcdn p (m × n) = gcdn p m.
+Lemma Gauss_gcdl p m n : coprime p n → gcdn p (m × n) = gcdn p m.

-Lemma coprime_mulr p m n : coprime p (m × n) = coprime p m && coprime p n.
+Lemma coprime_mulr p m n : coprime p (m × n) = coprime p m && coprime p n.

-Lemma coprime_mull p m n : coprime (m × n) p = coprime m p && coprime n p.
+Lemma coprime_mull p m n : coprime (m × n) p = coprime m p && coprime n p.

-Lemma coprime_pexpl k m n : 0 < k → coprime (m ^ k) n = coprime m n.
+Lemma coprime_pexpl k m n : 0 < k → coprime (m ^ k) n = coprime m n.

-Lemma coprime_pexpr k m n : 0 < k → coprime m (n ^ k) = coprime m n.
+Lemma coprime_pexpr k m n : 0 < k → coprime m (n ^ k) = coprime m n.

-Lemma coprime_expl k m n : coprime m n → coprime (m ^ k) n.
+Lemma coprime_expl k m n : coprime m n → coprime (m ^ k) n.

-Lemma coprime_expr k m n : coprime m n → coprime m (n ^ k).
+Lemma coprime_expr k m n : coprime m n → coprime m (n ^ k).

-Lemma coprime_dvdl m n p : m %| n → coprime n p → coprime m p.
+Lemma coprime_dvdl m n p : m %| n → coprime n p → coprime m p.

-Lemma coprime_dvdr m n p : m %| n → coprime p n → coprime p m.
+Lemma coprime_dvdr m n p : m %| n → coprime p n → coprime p m.

-Lemma coprime_egcdn n m : n > 0 → coprime (egcdn n m).1 (egcdn n m).2.
+Lemma coprime_egcdn n m : n > 0 → coprime (egcdn n m).1 (egcdn n m).2.

-Lemma dvdn_pexp2r m n k : k > 0 → (m ^ k %| n ^ k) = (m %| n).
+Lemma dvdn_pexp2r m n k : k > 0 → (m ^ k %| n ^ k) = (m %| n).

Section Chinese.
@@ -760,12 +759,12 @@

-Variables m1 m2 : nat.
+Variables m1 m2 : nat.
Hypothesis co_m12 : coprime m1 m2.

Lemma chinese_remainder x y :
-  (x == y %[mod m1 × m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
+  (x == y %[mod m1 × m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).

@@ -777,16 +776,16 @@
Definition chinese r1 r2 :=
-  r1 × m2 × (egcdn m2 m1).1 + r2 × m1 × (egcdn m1 m2).1.
+  r1 × m2 × (egcdn m2 m1).1 + r2 × m1 × (egcdn m1 m2).1.

-Lemma chinese_modl r1 r2 : chinese r1 r2 = r1 %[mod m1].
+Lemma chinese_modl r1 r2 : chinese r1 r2 = r1 %[mod m1].

-Lemma chinese_modr r1 r2 : chinese r1 r2 = r2 %[mod m2].
+Lemma chinese_modr r1 r2 : chinese r1 r2 = r2 %[mod m2].

-Lemma chinese_mod x : x = chinese (x %% m1) (x %% m2) %[mod m1 × m2].
+Lemma chinese_mod x : x = chinese (x %% m1) (x %% m2) %[mod m1 × m2].

End Chinese.
-- cgit v1.2.3