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.algebra.intdiv.html | 417 +++++++++++++++--------------- 1 file changed, 208 insertions(+), 209 deletions(-) (limited to 'docs/htmldoc/mathcomp.algebra.intdiv.html') diff --git a/docs/htmldoc/mathcomp.algebra.intdiv.html b/docs/htmldoc/mathcomp.algebra.intdiv.html index ccede4d..620b18d 100644 --- a/docs/htmldoc/mathcomp.algebra.intdiv.html +++ b/docs/htmldoc/mathcomp.algebra.intdiv.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.

@@ -73,111 +72,111 @@
Definition divz (m d : int) :=
-  let: (K, n) := match m with Posz n ⇒ (Posz, n) | Negz n ⇒ (Negz, n) end in
-  sgz d × K (n %/ `|d|)%N.
+  let: (K, n) := match m with Posz n ⇒ (Posz, n) | Negz n ⇒ (Negz, n) end in
+  sgz d × K (n %/ `|d|)%N.

-Definition modz (m d : int) : int := m - divz m d × d.
+Definition modz (m d : int) : int := m - divz m d × d.

-Definition dvdz d m := (`|d| %| `|m|)%N.
+Definition dvdz d m := (`|d| %| `|m|)%N.

-Definition gcdz m n := (gcdn `|m| `|n|)%:Z.
+Definition gcdz m n := (gcdn `|m| `|n|)%:Z.

-Definition egcdz m n : int × int :=
-  if m == 0 then (0, (-1) ^+ (n < 0)%R) else
-  let: (u, v) := egcdn `|m| `|n| in (sgz m × u, - (-1) ^+ (n < 0)%R × v%:Z).
+Definition egcdz m n : int × int :=
+  if m == 0 then (0, (-1) ^+ (n < 0)%R) else
+  let: (u, v) := egcdn `|m| `|n| in (sgz m × u, - (-1) ^+ (n < 0)%R × v%:Z).

-Definition coprimez m n := (gcdz m n == 1).
+Definition coprimez m n := (gcdz m n == 1).

-Infix "%/" := divz : int_scope.
-Infix "%%" := modz : int_scope.
-Notation "d %| m" := (m \in dvdz d) : int_scope.
-Notation "m = n %[mod d ]" := (modz m d = modz n d) : int_scope.
-Notation "m == n %[mod d ]" := (modz m d == modz n d) : int_scope.
-Notation "m <> n %[mod d ]" := (modz m d ≠ modz n d) : int_scope.
-Notation "m != n %[mod d ]" := (modz m d != modz n d) : int_scope.
+Infix "%/" := divz : int_scope.
+Infix "%%" := modz : int_scope.
+Notation "d %| m" := (m \in dvdz d) : int_scope.
+Notation "m = n %[mod d ]" := (modz m d = modz n d) : int_scope.
+Notation "m == n %[mod d ]" := (modz m d == modz n d) : int_scope.
+Notation "m <> n %[mod d ]" := (modz m d ≠ modz n d) : int_scope.
+Notation "m != n %[mod d ]" := (modz m d != modz n d) : int_scope.

-Lemma divz_nat (n d : nat) : (n %/ d)%Z = (n %/ d)%N.
+Lemma divz_nat (n d : nat) : (n %/ d)%Z = (n %/ d)%N.

-Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.
+Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.

-Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R × (m %/ d)%Z.
+Lemma divz_abs m d : (m %/ `|d|)%Z = (-1) ^+ (d < 0)%R × (m %/ d)%Z.

-Lemma div0z d : (0 %/ d)%Z = 0.
+Lemma div0z d : (0 %/ d)%Z = 0.

-Lemma divNz_nat m d : (d > 0)%N → (Negz m %/ d)%Z = - (m %/ d).+1%:Z.
+Lemma divNz_nat m d : (d > 0)%N → (Negz m %/ d)%Z = - (m %/ d).+1%:Z.

-Lemma divz_eq m d : m = (m %/ d)%Z × d + (m %% d)%Z.
+Lemma divz_eq m d : m = (m %/ d)%Z × d + (m %% d)%Z.

-Lemma modzN m d : (m %% - d)%Z = (m %% d)%Z.
+Lemma modzN m d : (m %% - d)%Z = (m %% d)%Z.

-Lemma modz_abs m d : (m %% `|d|%N)%Z = (m %% d)%Z.
+Lemma modz_abs m d : (m %% `|d|%N)%Z = (m %% d)%Z.

-Lemma modz_nat (m d : nat) : (m %% d)%Z = (m %% d)%N.
+Lemma modz_nat (m d : nat) : (m %% d)%Z = (m %% d)%N.

-Lemma modNz_nat m d : (d > 0)%N → (Negz m %% d)%Z = d%:Z - 1 - (m %% d)%:Z.
+Lemma modNz_nat m d : (d > 0)%N → (Negz m %% d)%Z = d%:Z - 1 - (m %% d)%:Z.

-Lemma modz_ge0 m d : d != 0 → 0 ≤ (m %% d)%Z.
+Lemma modz_ge0 m d : d != 0 → 0 ≤ (m %% d)%Z.

-Lemma divz0 m : (m %/ 0)%Z = 0.
-Lemma mod0z d : (0 %% d)%Z = 0.
-Lemma modz0 m : (m %% 0)%Z = m.
+Lemma divz0 m : (m %/ 0)%Z = 0.
+Lemma mod0z d : (0 %% d)%Z = 0.
+Lemma modz0 m : (m %% 0)%Z = m.

-Lemma divz_small m d : 0 ≤ m < `|d|%:Z → (m %/ d)%Z = 0.
+Lemma divz_small m d : 0 ≤ m < `|d|%:Z → (m %/ d)%Z = 0.

-Lemma divzMDl q m d : d != 0 → ((q × d + m) %/ d)%Z = q + (m %/ d)%Z.
+Lemma divzMDl q m d : d != 0 → ((q × d + m) %/ d)%Z = q + (m %/ d)%Z.

-Lemma mulzK m d : d != 0 → (m × d %/ d)%Z = m.
+Lemma mulzK m d : d != 0 → (m × d %/ d)%Z = m.

-Lemma mulKz m d : d != 0 → (d × m %/ d)%Z = m.
+Lemma mulKz m d : d != 0 → (d × m %/ d)%Z = m.

-Lemma expzB p m n : p != 0 → (m ≥ n)%N → p ^+ (m - n) = (p ^+ m %/ p ^+ n)%Z.
+Lemma expzB p m n : p != 0 → (m ≥ n)%N → p ^+ (m - n) = (p ^+ m %/ p ^+ n)%Z.

-Lemma modz1 m : (m %% 1)%Z = 0.
+Lemma modz1 m : (m %% 1)%Z = 0.

-Lemma divz1 m : (m %/ 1)%Z = m.
+Lemma divz1 m : (m %/ 1)%Z = m.

-Lemma divzz d : (d %/ d)%Z = (d != 0).
+Lemma divzz d : (d %/ d)%Z = (d != 0).

-Lemma ltz_pmod m d : d > 0 → (m %% d)%Z < d.
+Lemma ltz_pmod m d : d > 0 → (m %% d)%Z < d.

-Lemma ltz_mod m d : d != 0 → (m %% d)%Z < `|d|.
+Lemma ltz_mod m d : d != 0 → (m %% d)%Z < `|d|.

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

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

-Lemma lez_floor m d : d != 0 → (m %/ d)%Z × d ≤ m.
+Lemma lez_floor m d : d != 0 → (m %/ d)%Z × d ≤ m.

@@ -186,85 +185,85 @@ leq_mod does not extend to negative m.
-Lemma lez_div m d : (`|(m %/ d)%Z| ≤ `|m|)%N.
+Lemma lez_div m d : (`|(m %/ d)%Z| ≤ `|m|)%N.

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

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

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

-Lemma divz_ge0 m d : d > 0 → ((m %/ d)%Z ≥ 0) = (m ≥ 0).
+Lemma divz_ge0 m d : d > 0 → ((m %/ d)%Z ≥ 0) = (m ≥ 0).

-Lemma divzMA_ge0 m n p : n ≥ 0 → (m %/ (n × p) = (m %/ n)%Z %/ p)%Z.
+Lemma divzMA_ge0 m n p : n ≥ 0 → (m %/ (n × p) = (m %/ n)%Z %/ p)%Z.

-Lemma modz_small m d : 0 ≤ m < d → (m %% d)%Z = m.
+Lemma modz_small m d : 0 ≤ m < d → (m %% d)%Z = m.

-Lemma modz_mod m d : ((m %% d)%Z = m %[mod d])%Z.
+Lemma modz_mod m d : ((m %% d)%Z = m %[mod d])%Z.

-Lemma modzMDl p m d : (p × d + m = m %[mod d])%Z.
+Lemma modzMDl p m d : (p × d + m = m %[mod d])%Z.

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

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

-Lemma modzDl m d : (d + m = m %[mod d])%Z.
+Lemma modzDl m d : (d + m = m %[mod d])%Z.

-Lemma modzDr m d : (m + d = m %[mod d])%Z.
+Lemma modzDr m d : (m + d = m %[mod d])%Z.

-Lemma modzz d : (d %% d)%Z = 0.
+Lemma modzz d : (d %% d)%Z = 0.

-Lemma modzMl p d : (p × d %% d)%Z = 0.
+Lemma modzMl p d : (p × d %% d)%Z = 0.

-Lemma modzMr p d : (d × p %% d)%Z = 0.
+Lemma modzMr p d : (d × p %% d)%Z = 0.

-Lemma modzDml m n d : ((m %% d)%Z + n = m + n %[mod d])%Z.
+Lemma modzDml m n d : ((m %% d)%Z + n = m + n %[mod d])%Z.

-Lemma modzDmr m n d : (m + (n %% d)%Z = m + n %[mod d])%Z.
+Lemma modzDmr m n d : (m + (n %% d)%Z = m + n %[mod d])%Z.

-Lemma modzDm m n d : ((m %% d)%Z + (n %% d)%Z = m + n %[mod d])%Z.
+Lemma modzDm m n d : ((m %% d)%Z + (n %% d)%Z = m + n %[mod d])%Z.

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

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

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

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

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

-Lemma modzXm k m d : ((m %% d)%Z ^+ k = m ^+ k %[mod d])%Z.
+Lemma modzXm k m d : ((m %% d)%Z ^+ k = m ^+ k %[mod d])%Z.

-Lemma modzNm m d : (- (m %% d)%Z = - m %[mod d])%Z.
+Lemma modzNm m d : (- (m %% d)%Z = - m %[mod d])%Z.

-Lemma modz_absm m d : ((-1) ^+ (m < 0)%R × (m %% d)%Z = `|m|%:Z %[mod d])%Z.
+Lemma modz_absm m d : ((-1) ^+ (m < 0)%R × (m %% d)%Z = `|m|%:Z %[mod d])%Z.

@@ -275,93 +274,93 @@

-Fact dvdz_key d : pred_key (dvdz d).
-Canonical dvdz_keyed d := KeyedPred (dvdz_key d).
+Fact dvdz_key d : pred_key (dvdz d).
+Canonical dvdz_keyed d := KeyedPred (dvdz_key d).

-Lemma dvdzE d m : (d %| m)%Z = (`|d| %| `|m|)%N.
-Lemma dvdz0 d : (d %| 0)%Z.
-Lemma dvd0z n : (0 %| n)%Z = (n == 0).
-Lemma dvdz1 d : (d %| 1)%Z = (`|d|%N == 1%N).
-Lemma dvd1z m : (1 %| m)%Z.
-Lemma dvdzz m : (m %| m)%Z.
+Lemma dvdzE d m : (d %| m)%Z = (`|d| %| `|m|)%N.
+Lemma dvdz0 d : (d %| 0)%Z.
+Lemma dvd0z n : (0 %| n)%Z = (n == 0).
+Lemma dvdz1 d : (d %| 1)%Z = (`|d|%N == 1%N).
+Lemma dvd1z m : (1 %| m)%Z.
+Lemma dvdzz m : (m %| m)%Z.

-Lemma dvdz_mull d m n : (d %| n)%Z → (d %| m × n)%Z.
+Lemma dvdz_mull d m n : (d %| n)%Z → (d %| m × n)%Z.

-Lemma dvdz_mulr d m n : (d %| m)%Z → (d %| m × n)%Z.
- Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr.
+Lemma dvdz_mulr d m n : (d %| m)%Z → (d %| m × n)%Z.
+ Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr : core.

-Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2)%Z.
+Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2)%Z.

-Lemma dvdz_trans n d m : (d %| n → n %| m → d %| m)%Z.
+Lemma dvdz_trans n d m : (d %| n → n %| m → d %| m)%Z.

-Lemma dvdzP d m : reflect (∃ q, m = q × d) (d %| m)%Z.
+Lemma dvdzP d m : reflect (∃ q, m = q × d) (d %| m)%Z.

-Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
+Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.

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

-Lemma divzK d m : (d %| m)%Z → (m %/ d)%Z × d = m.
+Lemma divzK d m : (d %| m)%Z → (m %/ d)%Z × d = m.

-Lemma lez_divLR d m n : 0 < d → (d %| m)%Z → ((m %/ d)%Z ≤ n) = (m ≤ n × d).
+Lemma lez_divLR d m n : 0 < d → (d %| m)%Z → ((m %/ d)%Z ≤ n) = (m ≤ n × d).

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

-Lemma eqz_div d m n : d != 0 → (d %| m)%Z → (n == m %/ d)%Z = (n × d == m).
+Lemma eqz_div d m n : d != 0 → (d %| m)%Z → (n == m %/ d)%Z = (n × d == m).

-Lemma eqz_mul d m n : d != 0 → (d %| m)%Z → (m == n × d) = (m %/ d == n)%Z.
+Lemma eqz_mul d m n : d != 0 → (d %| m)%Z → (m == n × d) = (m %/ d == n)%Z.

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

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

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

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

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

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

-Lemma divzMl p m d : p != 0 → (d %| m → p × m %/ (p × d) = m %/ d)%Z.
+Lemma divzMl p m d : p != 0 → (d %| m → p × m %/ (p × d) = m %/ d)%Z.

-Lemma divzMr p m d : p != 0 → (d %| m → m × p %/ (d × p) = m %/ d)%Z.
+Lemma divzMr p m d : p != 0 → (d %| m → m × p %/ (d × p) = m %/ d)%Z.

-Lemma dvdz_mul2l p d m : p != 0 → (p × d %| p × m)%Z = (d %| m)%Z.
+Lemma dvdz_mul2l p d m : p != 0 → (p × d %| p × m)%Z = (d %| m)%Z.

-Lemma dvdz_mul2r p d m : p != 0 → (d × p %| m × p)%Z = (d %| m)%Z.
+Lemma dvdz_mul2r p d m : p != 0 → (d × p %| m × p)%Z = (d %| m)%Z.

-Lemma dvdz_exp2l p m n : (m ≤ n)%N → (p ^+ m %| p ^+ n)%Z.
+Lemma dvdz_exp2l p m n : (m ≤ n)%N → (p ^+ m %| p ^+ n)%Z.

-Lemma dvdz_Pexp2l p m n : `|p| > 1 → (p ^+ m %| p ^+ n)%Z = (m ≤ n)%N.
+Lemma dvdz_Pexp2l p m n : `|p| > 1 → (p ^+ m %| p ^+ n)%Z = (m ≤ n)%N.

-Lemma dvdz_exp2r m n k : (m %| n → m ^+ k %| n ^+ k)%Z.
+Lemma dvdz_exp2r m n k : (m %| n → m ^+ k %| n ^+ k)%Z.

Fact dvdz_zmod_closed d : zmod_closed (dvdz d).
@@ -370,24 +369,24 @@ Canonical dvdz_zmodPred d := ZmodPred (dvdz_zmod_closed d).

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

-Lemma eqz_mod_dvd d m n : (m == n %[mod d])%Z = (d %| m - n)%Z.
+Lemma eqz_mod_dvd d m n : (m == n %[mod d])%Z = (d %| m - n)%Z.

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

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

-Lemma Qint_dvdz (m d : int) : (d %| m)%Z → ((m%:~R / d%:~R : rat) \is a Qint).
+Lemma Qint_dvdz (m d : int) : (d %| m)%Z → ((m%:~R / d%:~R : rat) \is a Qint).

-Lemma Qnat_dvd (m d : nat) : (d %| m)%N → ((m%:R / d%:R : rat) \is a Qnat).
+Lemma Qnat_dvd (m d : nat) : (d %| m)%N → ((m%:R / d%:R : rat) \is a Qnat).

@@ -398,71 +397,71 @@

-Lemma gcdzz m : gcdz m m = `|m|%:Z.
-Lemma gcdzC : commutative gcdz.
-Lemma gcd0z m : gcdz 0 m = `|m|%:Z.
-Lemma gcdz0 m : gcdz m 0 = `|m|%:Z.
-Lemma gcd1z : left_zero 1 gcdz.
-Lemma gcdz1 : right_zero 1 gcdz.
-Lemma dvdz_gcdr m n : (gcdz m n %| n)%Z.
-Lemma dvdz_gcdl m n : (gcdz m n %| m)%Z.
-Lemma gcdz_eq0 m n : (gcdz m n == 0) = (m == 0) && (n == 0).
- Lemma gcdNz m n : gcdz (- m) n = gcdz m n.
-Lemma gcdzN m n : gcdz m (- n) = gcdz m n.
+Lemma gcdzz m : gcdz m m = `|m|%:Z.
+Lemma gcdzC : commutative gcdz.
+Lemma gcd0z m : gcdz 0 m = `|m|%:Z.
+Lemma gcdz0 m : gcdz m 0 = `|m|%:Z.
+Lemma gcd1z : left_zero 1 gcdz.
+Lemma gcdz1 : right_zero 1 gcdz.
+Lemma dvdz_gcdr m n : (gcdz m n %| n)%Z.
+Lemma dvdz_gcdl m n : (gcdz m n %| m)%Z.
+Lemma gcdz_eq0 m n : (gcdz m n == 0) = (m == 0) && (n == 0).
+ Lemma gcdNz m n : gcdz (- m) n = gcdz m n.
+Lemma gcdzN m n : gcdz m (- n) = gcdz m n.

-Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.
+Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.

-Lemma gcdz_modl m n : gcdz (m %% n)%Z n = gcdz m n.
+Lemma gcdz_modl m n : gcdz (m %% n)%Z n = gcdz m n.

-Lemma gcdzMDl q m n : gcdz m (q × m + n) = gcdz m n.
+Lemma gcdzMDl q m n : gcdz m (q × m + n) = gcdz m n.

-Lemma gcdzDl m n : gcdz m (m + n) = gcdz m n.
+Lemma gcdzDl m n : gcdz m (m + n) = gcdz m n.

-Lemma gcdzDr m n : gcdz m (n + m) = gcdz m n.
+Lemma gcdzDr m n : gcdz m (n + m) = gcdz m n.

-Lemma gcdzMl n m : gcdz n (m × n) = `|n|%:Z.
+Lemma gcdzMl n m : gcdz n (m × n) = `|n|%:Z.

-Lemma gcdzMr n m : gcdz n (n × m) = `|n|%:Z.
+Lemma gcdzMr n m : gcdz n (n × m) = `|n|%:Z.

-Lemma gcdz_idPl {m n} : reflect (gcdz m n = `|m|%:Z) (m %| n)%Z.
+Lemma gcdz_idPl {m n} : reflect (gcdz m n = `|m|%:Z) (m %| n)%Z.

-Lemma gcdz_idPr {m n} : reflect (gcdz m n = `|n|%:Z) (n %| m)%Z.
+Lemma gcdz_idPr {m n} : reflect (gcdz m n = `|n|%:Z) (n %| m)%Z.

-Lemma expz_min e m n : e ≥ 0 → e ^+ minn m n = gcdz (e ^+ m) (e ^+ n).
+Lemma expz_min e m n : e ≥ 0 → e ^+ minn m n = gcdz (e ^+ m) (e ^+ n).

-Lemma dvdz_gcd p m n : (p %| gcdz m n)%Z = (p %| m)%Z && (p %| n)%Z.
+Lemma dvdz_gcd p m n : (p %| gcdz m n)%Z = (p %| m)%Z && (p %| n)%Z.

-Lemma gcdzAC : right_commutative gcdz.
+Lemma gcdzAC : right_commutative gcdz.

-Lemma gcdzA : associative gcdz.
+Lemma gcdzA : associative gcdz.

-Lemma gcdzCA : left_commutative gcdz.
+Lemma gcdzCA : left_commutative gcdz.

-Lemma gcdzACA : interchange gcdz gcdz.
+Lemma gcdzACA : interchange gcdz gcdz.

-Lemma mulz_gcdr m n p : `|m|%:Z × gcdz n p = gcdz (m × n) (m × p).
+Lemma mulz_gcdr m n p : `|m|%:Z × gcdz n p = gcdz (m × n) (m × p).

-Lemma mulz_gcdl m n p : gcdz m n × `|p|%:Z = gcdz (m × p) (n × p).
+Lemma mulz_gcdl m n p : gcdz m n × `|p|%:Z = gcdz (m × p) (n × p).

-Lemma mulz_divCA_gcd n m : n × (m %/ gcdz n m)%Z = m × (n %/ gcdz n m)%Z.
+Lemma mulz_divCA_gcd n m : n × (m %/ gcdz n m)%Z = m × (n %/ gcdz n m)%Z.

@@ -476,74 +475,74 @@

-Lemma coprimezE m n : coprimez m n = coprime `|m| `|n|.
+Lemma coprimezE m n : coprimez m n = coprime `|m| `|n|.

-Lemma coprimez_sym : symmetric coprimez.
+Lemma coprimez_sym : symmetric coprimez.

-Lemma coprimeNz m n : coprimez (- m) n = coprimez m n.
+Lemma coprimeNz m n : coprimez (- m) n = coprimez m n.

-Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
+Lemma coprimezN m n : coprimez m (- n) = coprimez m n.

-CoInductive egcdz_spec m n : int × int → Type :=
-  EgcdzSpec u v of u × m + v × n = gcdz m n & coprimez u v
-     : egcdz_spec m n (u, v).
+Variant egcdz_spec m n : int × int → Type :=
+  EgcdzSpec u v of u × m + v × n = gcdz m n & coprimez u v
+     : egcdz_spec m n (u, v).

Lemma egcdzP m n : egcdz_spec m n (egcdz m n).

-Lemma Bezoutz m n : {u : int & {v : int | u × m + v × n = gcdz m n}}.
+Lemma Bezoutz m n : {u : int & {v : int | u × m + v × n = gcdz m n}}.

Lemma coprimezP m n :
-  reflect (∃ uv, uv.1 × m + uv.2 × n = 1) (coprimez m n).
+  reflect (∃ uv, uv.1 × m + uv.2 × n = 1) (coprimez m n).

Lemma Gauss_dvdz m n p :
-  coprimez m n → (m × n %| p)%Z = (m %| p)%Z && (n %| p)%Z.
+  coprimez m n → (m × n %| p)%Z = (m %| p)%Z && (n %| p)%Z.

-Lemma Gauss_dvdzr m n p : coprimez m n → (m %| n × p)%Z = (m %| p)%Z.
+Lemma Gauss_dvdzr m n p : coprimez m n → (m %| n × p)%Z = (m %| p)%Z.

-Lemma Gauss_dvdzl m n p : coprimez m p → (m %| n × p)%Z = (m %| n)%Z.
+Lemma Gauss_dvdzl m n p : coprimez m p → (m %| n × p)%Z = (m %| n)%Z.

-Lemma Gauss_gcdzr p m n : coprimez p m → gcdz p (m × n) = gcdz p n.
+Lemma Gauss_gcdzr p m n : coprimez p m → gcdz p (m × n) = gcdz p n.

-Lemma Gauss_gcdzl p m n : coprimez p n → gcdz p (m × n) = gcdz p m.
+Lemma Gauss_gcdzl p m n : coprimez p n → gcdz p (m × n) = gcdz p m.

-Lemma coprimez_mulr p m n : coprimez p (m × n) = coprimez p m && coprimez p n.
+Lemma coprimez_mulr p m n : coprimez p (m × n) = coprimez p m && coprimez p n.

-Lemma coprimez_mull p m n : coprimez (m × n) p = coprimez m p && coprimez n p.
+Lemma coprimez_mull p m n : coprimez (m × n) p = coprimez m p && coprimez n p.

-Lemma coprimez_pexpl k m n : (0 < k)%N → coprimez (m ^+ k) n = coprimez m n.
+Lemma coprimez_pexpl k m n : (0 < k)%N → coprimez (m ^+ k) n = coprimez m n.

-Lemma coprimez_pexpr k m n : (0 < k)%N → coprimez m (n ^+ k) = coprimez m n.
+Lemma coprimez_pexpr k m n : (0 < k)%N → coprimez m (n ^+ k) = coprimez m n.

-Lemma coprimez_expl k m n : coprimez m n → coprimez (m ^+ k) n.
+Lemma coprimez_expl k m n : coprimez m n → coprimez (m ^+ k) n.

-Lemma coprimez_expr k m n : coprimez m n → coprimez m (n ^+ k).
+Lemma coprimez_expr k m n : coprimez m n → coprimez m (n ^+ k).

-Lemma coprimez_dvdl m n p : (m %| n)%N → coprimez n p → coprimez m p.
+Lemma coprimez_dvdl m n p : (m %| n)%N → coprimez n p → coprimez m p.

-Lemma coprimez_dvdr m n p : (m %| n)%N → coprimez p n → coprimez p m.
+Lemma coprimez_dvdr m n p : (m %| n)%N → coprimez p n → coprimez p m.

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

Section Chinese.
@@ -562,7 +561,7 @@
Lemma zchinese_remainder x y :
-  (x == y %[mod m1 × m2])%Z = (x == y %[mod m1])%Z && (x == y %[mod m2])%Z.
+  (x == y %[mod m1 × m2])%Z = (x == y %[mod m1])%Z && (x == y %[mod m2])%Z.

@@ -574,16 +573,16 @@
Definition zchinese r1 r2 :=
-  r1 × m2 × (egcdz m1 m2).2 + r2 × m1 × (egcdz m1 m2).1.
+  r1 × m2 × (egcdz m1 m2).2 + r2 × m1 × (egcdz m1 m2).1.

-Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1])%Z.
+Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1])%Z.

-Lemma zchinese_modr r1 r2 : (zchinese r1 r2 = r2 %[mod m2])%Z.
+Lemma zchinese_modr r1 r2 : (zchinese r1 r2 = r2 %[mod m2])%Z.

-Lemma zchinese_mod x : (x = zchinese (x %% m1)%Z (x %% m2)%Z %[mod m1 × m2])%Z.
+Lemma zchinese_mod x : (x = zchinese (x %% m1)%Z (x %% m2)%Z %[mod m1 × m2])%Z.

End Chinese.
@@ -593,98 +592,98 @@
Definition zcontents p :=
-  sgz (lead_coef p) × \big[gcdn/0%N]_(i < size p) `|(p`_i)%R|%N.
+  sgz (lead_coef p) × \big[gcdn/0%N]_(i < size p) `|(p`_i)%R|%N.

-Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).
+Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).

-Lemma zcontents_eq0 p : (zcontents p == 0) = (p == 0).
+Lemma zcontents_eq0 p : (zcontents p == 0) = (p == 0).

-Lemma zcontents0 : zcontents 0 = 0.
+Lemma zcontents0 : zcontents 0 = 0.

-Lemma zcontentsZ a p : zcontents (a *: p) = a × zcontents p.
+Lemma zcontentsZ a p : zcontents (a *: p) = a × zcontents p.

-Lemma zcontents_monic p : p \is monic → zcontents p = 1.
+Lemma zcontents_monic p : p \is monic → zcontents p = 1.

-Lemma dvdz_contents a p : (a %| zcontents p)%Z = (p \is a polyOver (dvdz a)).
+Lemma dvdz_contents a p : (a %| zcontents p)%Z = (p \is a polyOver (dvdz a)).

-Lemma map_poly_divzK a p :
-  p \is a polyOver (dvdz a) → a *: map_poly (divz^~ a) p = p.
+Lemma map_poly_divzK {a} p :
+  p \is a polyOver (dvdz a) → a *: map_poly (divz^~ a) p = p.

Lemma polyOver_dvdzP a p :
-  reflect (∃ q, p = a *: q) (p \is a polyOver (dvdz a)).
+  reflect (∃ q, p = a *: q) (p \is a polyOver (dvdz a)).

-Definition zprimitive p := map_poly (divz^~ (zcontents p)) p.
+Definition zprimitive p := map_poly (divz^~ (zcontents p)) p.

-Lemma zpolyEprim p : p = zcontents p *: zprimitive p.
+Lemma zpolyEprim p : p = zcontents p *: zprimitive p.

-Lemma zprimitive0 : zprimitive 0 = 0.
+Lemma zprimitive0 : zprimitive 0 = 0.

-Lemma zprimitive_eq0 p : (zprimitive p == 0) = (p == 0).
+Lemma zprimitive_eq0 p : (zprimitive p == 0) = (p == 0).

-Lemma size_zprimitive p : size (zprimitive p) = size p.
+Lemma size_zprimitive p : size (zprimitive p) = size p.

-Lemma sgz_lead_primitive p : sgz (lead_coef (zprimitive p)) = (p != 0).
+Lemma sgz_lead_primitive p : sgz (lead_coef (zprimitive p)) = (p != 0).

-Lemma zcontents_primitive p : zcontents (zprimitive p) = (p != 0).
+Lemma zcontents_primitive p : zcontents (zprimitive p) = (p != 0).

-Lemma zprimitive_id p : zprimitive (zprimitive p) = zprimitive p.
+Lemma zprimitive_id p : zprimitive (zprimitive p) = zprimitive p.

-Lemma zprimitive_monic p : p \in monic → zprimitive p = p.
+Lemma zprimitive_monic p : p \in monic → zprimitive p = p.

-Lemma zprimitiveZ a p : a != 0 → zprimitive (a *: p) = zprimitive p.
+Lemma zprimitiveZ a p : a != 0 → zprimitive (a *: p) = zprimitive p.

Lemma zprimitive_min p a q :
-    p != 0 → p = a *: q →
-  {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p}.
+    p != 0 → p = a *: q →
+  {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p}.

Lemma zprimitive_irr p a q :
-  p != 0 → zprimitive p = a *: q → a = sgz (lead_coef q).
+  p != 0 → zprimitive p = a *: q → a = sgz (lead_coef q).

-Lemma zcontentsM p q : zcontents (p × q) = zcontents p × zcontents q.
+Lemma zcontentsM p q : zcontents (p × q) = zcontents p × zcontents q.

-Lemma zprimitiveM p q : zprimitive (p × q) = zprimitive p × zprimitive q.
+Lemma zprimitiveM p q : zprimitive (p × q) = zprimitive p × zprimitive q.

-Lemma dvdpP_int p q : p %| q → {r | q = zprimitive p × r}.
+Lemma dvdpP_int p q : p %| q → {r | q = zprimitive p × r}.


-Lemma size_rat_int_poly p : size (pZtoQ p) = size p.
+Lemma size_rat_int_poly p : size (pZtoQ p) = size p.

-Lemma rat_poly_scale (p : {poly rat}) :
-  {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}.
+Lemma rat_poly_scale (p : {poly rat}) :
+  {q : {poly int} & {a | a != 0 & p = a%:~R^-1 *: pZtoQ q}}.

-Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q) = (p %| q).
+Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q) = (p %| q).

Lemma dvdpP_rat_int p q :
-    p %| pZtoQ q →
-  {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 × r}}.
+    p %| pZtoQ q →
+  {p1 : {poly int} & {a | a != 0 & p = a *: pZtoQ p1} & {r | q = p1 × r}}.

End ZpolyScale.
@@ -698,19 +697,19 @@

-Lemma int_Smith_normal_form m n (M : 'M[int]_(m, n)) :
-  {L : 'M[int]_m & L \in unitmx &
-  {R : 'M[int]_n & R \in unitmx &
-  {d : seq int | sorted dvdz d &
-   M = L ×m (\matrix_(i, j) (d`_i *+ (i == j :> nat))) ×m R}}}.
+Lemma int_Smith_normal_form m n (M : 'M[int]_(m, n)) :
+  {L : 'M[int]_m & L \in unitmx &
+  {R : 'M[int]_n & R \in unitmx &
+  {d : seq int | sorted dvdz d &
+   M = L ×m (\matrix_(i, j) (d`_i *+ (i == j :> nat))) ×m R}}}.

-Definition inIntSpan (V : zmodType) m (s : m.-tuple V) v :=
-  ∃ a : int ^ m, v = \sum_(i < m) s`_i *~ a i.
+Definition inIntSpan (V : zmodType) m (s : m.-tuple V) v :=
+  ∃ a : int ^ m, v = \sum_(i < m) s`_i *~ a i.

-Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v :
-  decidable (inIntSpan s v).
+Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v :
+  decidable (inIntSpan s v).

-- cgit v1.2.3