+ +

Library mathcomp.algebra.ssrint

+ +

+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+Import GRing.Theory Num.Theory.
+ +
+

+ +

+ This file develops a basic theory of signed integers, defining: + int == the type of signed integers, with two constructors Posz for + non-negative integers and Negz for negative integers. It + supports the realDomainType interface (and its parents). + n%:Z == explicit cast from nat to int (:= Posz n); displayed as n. + However (Posz m = Posz n) is displayed as (m = n :> int) + (and so are ==, != and <>) + Lemma NegzE : turns (Negz n) into - n.+1%:Z. + x *~ m == m times x, with m : int; + convertible to x *+ n if m is Posz n + convertible to x *- n.+1 if m is Negz n. + m%:~R == the image of m : int in a generic ring (:= 1 *~ m). + x ^ m == x to the m, with m : int; + convertible to x ^+ n if m is Posz n + convertible to x ^- n.+1 if m is Negz n. + sgz x == sign of x : R, + equals (0 : int) if and only x == 0, + equals (1 : int) if x is positive + and (-1 : int) otherwise. + `|m|%N == the n : nat such that `|m|%R = n%:Z, for m : int. + `|m - n|%N == the distance between m and n; the '-' is specialized to + the int type, so m and n can be either of type nat or int + thanks to the Posz coercion; m and n are however parsed in + the %N scope. The IntDist submodule provides this notation + and the corresponding theory independently of the rest of + of the int and ssralg libraries (and notations). + Warning: due to the declaration of Posz as a coercion, two terms might be + displayed the same while not being convertible, for instance: + (Posz (x - y)) and (Posz x) - (Posz y) for x, y : nat. +

+ +
+Set Implicit Arguments.
+ +
+Delimit Scope int_scope with Z.
+Local Open Scope int_scope.
+ +
+

+ +

+ Defining int +

+CoInductive int : Set := Posz of nat | Negz of nat.
+

+ +

+ This must be deferred to module DistInt to work around the design flaws of + the Coq module system. + Coercion Posz : nat >-> int. +

+ +
+Notation "n %:Z" := (Posz n)
+  (at level 2, left associativity, format "n %:Z", only parsing) : int_scope.
+Notation "n %:Z" := (Posz n)
+  (at level 2, left associativity, format "n %:Z", only parsing) : ring_scope.
+ +
+Notation "n = m :> 'in' 't'" := (Posz n = Posz m)
+  (at level 70, m at next level, format "n = m :> 'in' 't'") : ring_scope.
+Notation "n == m :> 'in' 't'" := (Posz n == Posz m)
+  (at level 70, m at next level, format "n == m :> 'in' 't'") : ring_scope.
+Notation "n != m :> 'in' 't'" := (Posz n != Posz m)
+  (at level 70, m at next level, format "n != m :> 'in' 't'") : ring_scope.
+Notation "n <> m :> 'in' 't'" := (Posz n ≠ Posz m)
+  (at level 70, m at next level, format "n <> m :> 'in' 't'") : ring_scope.
+ +
+Definition natsum_of_int (m : int) : nat + nat :=
+  match m with Posz p ⇒ inl _ p | Negz n ⇒ inr _ n end.
+ +
+Definition int_of_natsum (m : nat + nat) :=
+  match m with inl p ⇒ Posz p | inr n ⇒ Negz n end.
+ +
+Lemma natsum_of_intK : cancel natsum_of_int int_of_natsum.
+ +
+Definition int_eqMixin := CanEqMixin natsum_of_intK.
+Definition int_countMixin := CanCountMixin natsum_of_intK.
+Definition int_choiceMixin := CountChoiceMixin int_countMixin.
+Canonical int_eqType := Eval hnf in EqType int int_eqMixin.
+Canonical int_choiceType := Eval hnf in ChoiceType int int_choiceMixin.
+Canonical int_countType := Eval hnf in CountType int int_countMixin.
+ +
+Lemma eqz_nat (m n : nat) : (m %:Z == n %:Z ) = (m == n ).
+ +
+Module intZmod.
+Section intZmod.
+ +
+Definition addz (m n : int) :=
+  match m, n with
+    | Posz m', Posz n' ⇒ Posz (m' + n')
+    | Negz m', Negz n' ⇒ Negz (m' + n').+1
+    | Posz m', Negz n' ⇒ if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
+    | Negz n', Posz m' ⇒ if n' < m' then Posz (m' - n'.+1) else Negz (n' - m')
+  end.
+ +
+Definition oppz m := nosimpl
+  match m with
+    | Posz n ⇒ if n is (n'.+1)%N then Negz n' else Posz 0
+    | Negz n ⇒ Posz (n.+1)%N
+  end.
+ +
+ +
+Lemma PoszD : {morph Posz : m n / (m + n)%N >-> m + n }.
+ +
+ +
+Lemma NegzE (n : nat) : Negz n = - n .+1.
+ +
+Lemma int_rect (P : int → Type) :
+  P 0 → (∀ n : nat, P n → P (n .+1))
+  → (∀ n : nat, P (- n) → P (- (n .+1 )))
+  → ∀ n : int, P n.
+ +
+Definition int_rec := int_rect.
+Definition int_ind := int_rect.
+ +
+CoInductive int_spec (x : int) : int → Type :=
+| ZintNull of x = 0 : int_spec x 0
+| ZintPos n of x = n .+1 : int_spec x n .+1
+| ZintNeg n of x = - (n .+1 )%:Z : int_spec x (- n .+1).
+ +
+Lemma intP x : int_spec x x.
+ +
+Lemma addzC : commutative addz.
+ +
+Lemma add0z : left_id 0 addz.
+ +
+Lemma oppzK : involutive oppz.
+ +
+Lemma oppz_add : {morph oppz : m n / m + n }.
+ +
+Lemma add1Pz (n : int) : 1 + (n - 1) = n.
+ +
+Lemma subSz1 (n : int) : 1 + n - 1 = n.
+ +
+Lemma addSnz (m : nat) (n : int) : (m .+1%N) + n = 1 + (m + n ).
+ +
+Lemma addSz (m n : int) : (1 + m ) + n = 1 + (m + n ).
+ +
+Lemma addPz (m n : int) : (m - 1) + n = (m + n ) - 1.
+ +
+Lemma addzA : associative addz.
+ +
+Lemma addNz : left_inverse (0:int) oppz addz.
+ +
+Lemma predn_int (n : nat) : 0 < n → n .-1 %:Z = n - 1.
+ +
+Definition Mixin := ZmodMixin addzA addzC add0z addNz.
+ +
+End intZmod.
+End intZmod.
+ +
+Canonical int_ZmodType := ZmodType int intZmod.Mixin.
+ +
+Local Open Scope ring_scope.
+ +
+Section intZmoduleTheory.
+ +
+ +
+Lemma PoszD : {morph Posz : n m / (n + m)%N >-> n + m }.
+ +
+Lemma NegzE (n : nat) : Negz n = -(n .+1 )%:Z.
+ +
+Lemma int_rect (P : int → Type) :
+  P 0 → (∀ n : nat, P n → P (n .+1)%N)
+  → (∀ n : nat, P (- (n %:Z )) → P (- (n .+1%N%:Z )))
+  → ∀ n : int, P n.
+ +
+Definition int_rec := int_rect.
+Definition int_ind := int_rect.
+ +
+CoInductive int_spec (x : int) : int → Type :=
+| ZintNull : int_spec x 0
+| ZintPos n : int_spec x n .+1
+| ZintNeg n : int_spec x (- (n .+1 )%:Z).
+ +
+Lemma intP x : int_spec x x.
+ +
+Definition oppz_add := (@opprD [zmodType of int ]).
+ +
+Lemma subzn (m n : nat) : (n ≤ m)%N → m %:Z - n %:Z = (m - n)%N.
+ +
+Lemma subzSS (m n : nat) : m .+1 %:Z - n .+1 %:Z = m %:Z - n %:Z.
+ +
+End intZmoduleTheory.
+ +
+Module intRing.
+Section intRing.
+ +
+ +
+Definition mulz (m n : int) :=
+  match m, n with
+    | Posz m', Posz n' ⇒ (m' × n')%N%:Z
+    | Negz m', Negz n' ⇒ (m'.+1%N × n'.+1%N)%N%:Z
+    | Posz m', Negz n' ⇒ - (m' × (n'.+1%N))%N%:Z
+    | Negz n', Posz m' ⇒ - (m' × (n'.+1%N))%N%:Z
+  end.
+ +
+ +
+Lemma mul0z : left_zero 0 *%Z.
+ +
+Lemma mulzC : commutative mulz.
+ +
+Lemma mulz0 : right_zero 0 *%Z.
+ +
+Lemma mulzN (m n : int) : (m × (- n ))%Z = - (m × n)%Z.
+ +
+Lemma mulNz (m n : int) : ((- m ) × n)%Z = - (m × n)%Z.
+ +
+Lemma mulzA : associative mulz.
+ +
+Lemma mul1z : left_id 1%Z mulz.
+ +
+Lemma mulzS (x : int) (n : nat) : (x × n .+1 %:Z)%Z = x + (x × n)%Z.
+ +
+Lemma mulz_addl : left_distributive mulz (+%R).
+ +
+Lemma nonzero1z : 1%Z != 0.
+ +
+Definition comMixin := ComRingMixin mulzA mulzC mul1z mulz_addl nonzero1z.
+ +
+End intRing.
+End intRing.
+ +
+Canonical int_Ring := Eval hnf in RingType int intRing.comMixin.
+Canonical int_comRing := Eval hnf in ComRingType int intRing.mulzC.
+ +
+Section intRingTheory.
+ +
+Implicit Types m n : int.
+ +
+Lemma PoszM : {morph Posz : n m / (n × m)%N >-> n × m }.
+ +
+Lemma intS (n : nat) : n .+1 %:Z = 1 + n %:Z.
+ +
+Lemma predn_int (n : nat) : (0 < n)%N → n .-1 %:Z = n %:Z - 1.
+ +
+End intRingTheory.
+ +
+Module intUnitRing.
+Section intUnitRing.
+Implicit Types m n : int.
+ +
+Definition unitz := [qualify a n : int | (n == 1) || (n == -1)].
+Definition invz n : int := n.
+ +
+Lemma mulVz : {in unitz , left_inverse 1%R invz *%R }.
+ +
+Lemma mulzn_eq1 m (n : nat) : (m × n == 1) = (m == 1) && (n == 1%N).
+ +
+Lemma unitzPl m n : n × m = 1 → m \is a unitz.
+ +
+Lemma invz_out : {in [predC unitz ], invz =1 id }.
+ +
+Lemma idomain_axiomz m n : m × n = 0 → (m == 0) || (n == 0).
+ +
+Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out.
+ +
+End intUnitRing.
+End intUnitRing.
+ +
+Canonical int_unitRingType :=
+  Eval hnf in UnitRingType int intUnitRing.comMixin.
+Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int ].
+Canonical int_iDomain :=
+  Eval hnf in IdomainType int intUnitRing.idomain_axiomz.
+ +
+Definition absz m := match m with Posz p ⇒ p | Negz n ⇒ n.+1 end.
+Notation "m - n" :=
+  (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
+ +
+Module intOrdered.
+Section intOrdered.
+Implicit Types m n p : int.
+ +
+ +
+Definition lez m n :=
+  match m, n with
+    | Posz m', Posz n' ⇒ (m' ≤ n')%N
+    | Posz m', Negz n' ⇒ false
+    | Negz m', Posz n' ⇒ true
+    | Negz m', Negz n' ⇒ (n' ≤ m')%N
+  end.
+ +
+Definition ltz m n :=
+  match m, n with
+    | Posz m', Posz n' ⇒ (m' < n')%N
+    | Posz m', Negz n' ⇒ false
+    | Negz m', Posz n' ⇒ true
+    | Negz m', Negz n' ⇒ (n' < m')%N
+  end.
+ +
+Fact lez_norm_add x y : lez (normz (x + y)) (normz x + normz y).
+ +
+Fact ltz_add x y : ltz 0 x → ltz 0 y → ltz 0 (x + y).
+ +
+Fact eq0_normz x : normz x = 0 → x = 0.
+ +
+Fact lez_total x y : lez x y || lez y x.
+ +
+Lemma abszN (n : nat) : absz (- n %:Z) = n.
+ +
+Fact normzM : {morph (fun n ⇒ normz n ) : x y / x × y }.
+ +
+Lemma subz_ge0 m n : lez 0 (n - m) = lez m n.
+ +
+Fact lez_def x y : (lez x y ) = (normz (y - x) == y - x ).
+ +
+Fact ltz_def x y : (ltz x y ) = (y != x ) && (lez x y ).
+ +
+Definition Mixin :=
+   NumMixin lez_norm_add ltz_add eq0_normz (in2W lez_total) normzM
+            lez_def ltz_def.
+ +
+End intOrdered.
+End intOrdered.
+ +
+Canonical int_numDomainType := NumDomainType int intOrdered.Mixin.
+Canonical int_realDomainType := RealDomainType int (intOrdered.lez_total 0).
+ +
+Section intOrderedTheory.
+ +
+Implicit Types m n p : nat.
+Implicit Types x y z : int.
+ +
+Lemma lez_nat m n : (m ≤ n :> int ) = (m ≤ n)%N.
+ +
+Lemma ltz_nat m n : (m < n :> int ) = (m < n)%N.
+ +
+Definition ltez_nat := (lez_nat , ltz_nat ).
+ +
+Lemma leNz_nat m n : (- m %:Z ≤ n).
+ +
+Lemma ltNz_nat m n : (- m %:Z < n ) = (m != 0%N) || (n != 0%N).
+ +
+Definition lteNz_nat := (leNz_nat , ltNz_nat ).
+ +
+Lemma lezN_nat m n : (m %:Z ≤ - n %:Z ) = (m == 0%N) && (n == 0%N).
+ +
+Lemma ltzN_nat m n : (m %:Z < - n %:Z ) = false.
+ +
+Lemma le0z_nat n : 0 ≤ n :> int.
+ +
+Lemma lez0_nat n : n ≤ 0 :> int = (n == 0%N :> nat ).
+ +
+Definition ltezN_nat := (lezN_nat , ltzN_nat ).
+Definition ltez_natE := (ltez_nat , lteNz_nat , ltezN_nat , le0z_nat , lez0_nat ).
+ +
+Lemma gtz0_ge1 x : (0 < x ) = (1 ≤ x ).
+ +
+Lemma lez_add1r x y : (1 + x ≤ y ) = (x < y ).
+ +
+Lemma lez_addr1 x y : (x + 1 ≤ y ) = (x < y ).
+ +
+Lemma ltz_add1r x y : (x < 1 + y ) = (x ≤ y ).
+ +
+Lemma ltz_addr1 x y : (x < y + 1) = (x ≤ y ).
+ +
+End intOrderedTheory.
+ +
+ +
+

+ +

+ definition of intmul +

+Definition intmul (R : zmodType) (x : R) (n : int) := nosimpl
+  match n with
+    | Posz n ⇒ (x *+ n)%R
+    | Negz n ⇒ (x *- (n .+1 ))%R
+  end.
+ +
+Notation "*~%R" := (@intmul _) (at level 0, format " *~%R") : ring_scope.
+Notation "x *~ n" := (intmul x n)
+  (at level 40, left associativity, format "x *~ n") : ring_scope.
+Notation intr := ( *~%R 1).
+Notation "n %:~R" := (1 *~ n)%R
+  (at level 2, left associativity, format "n %:~R") : ring_scope.
+ +
+Lemma pmulrn (R : zmodType) (x : R) (n : nat) : x *+ n = x *~ n %:Z.
+ +
+Lemma nmulrn (R : zmodType) (x : R) (n : nat) : x *- n = x *~ - n %:Z.
+ +
+Section ZintLmod.
+ +
+Definition zmodule (M : Type) : Type := M.
+ +
+Variable M : zmodType.
+ +
+Implicit Types m n : int.
+Implicit Types x y z : M.
+ +
+Fact mulrzA_C m n x : (x *~ n ) *~ m = x *~ (m × n ).
+ +
+Fact mulrzAC m n x : (x *~ n ) *~ m = (x *~ m ) *~ n.
+ +
+Fact mulr1z (x : M) : x *~ 1 = x.
+ +
+Fact mulrzDr m : {morph ( *~%R ^~ m : M → M ) : x y / x + y }.
+ +
+Lemma mulrzBl_nat (m n : nat) x : x *~ (m %:Z - n %:Z ) = x *~ m - x *~ n.
+ +
+Fact mulrzDl x : {morph *~%R x : m n / m + n }.
+ +
+Definition Mint_LmodMixin :=
+  @LmodMixin _ [zmodType of M ] (fun n x ⇒ x *~ n)
+   mulrzA_C mulr1z mulrzDr mulrzDl.
+Canonical Mint_LmodType := LmodType int M ^z Mint_LmodMixin.
+ +
+Lemma scalezrE n x : n *: (x : M ^z ) = x *~ n.
+ +
+Lemma mulrzA x m n : x *~ (m × n ) = x *~ m *~ n.
+ +
+Lemma mulr0z x : x *~ 0 = 0.
+ +
+Lemma mul0rz n : 0 *~ n = 0 :> M.
+ +
+Lemma mulrNz x n : x *~ (- n ) = - (x *~ n ).
+ +
+Lemma mulrN1z x : x *~ (- 1) = - x.
+ +
+Lemma mulNrz x n : (- x ) *~ n = - (x *~ n ).
+ +
+Lemma mulrzBr x m n : x *~ (m - n ) = x *~ m - x *~ n.
+ +
+Lemma mulrzBl x y n : (x - y ) *~ n = x *~ n - y *~ n.
+ +
+Lemma mulrz_nat (n : nat) x : x *~ n %:R = x *+ n.
+ +
+Lemma mulrz_sumr : ∀ x I r (P : pred I) F,
+  x *~ (\sum_(i <- r | P i ) F i ) = \sum_(i <- r | P i ) x *~ F i.
+ +
+Lemma mulrz_suml : ∀ n I r (P : pred I) (F : I → M),
+  (\sum_(i <- r | P i ) F i ) *~ n = \sum_(i <- r | P i ) F i *~ n.
+ +
+Canonical intmul_additive x := Additive (@mulrzBr x).
+ +
+End ZintLmod.
+ +
+Lemma ffunMzE (I : finType) (M : zmodType) (f : {ffun I → M }) z x :
+  (f *~ z) x = f x *~ z.
+ +
+Lemma intz (n : int) : n %:~R = n.
+ +
+Lemma natz (n : nat) : n %:R = n %:Z :> int.
+ +
+Section RintMod.
+ +
+Variable R : ringType.
+ +
+Implicit Types m n : int.
+Implicit Types x y z : R.
+ +
+Lemma mulrzAl n x y : (x *~ n ) × y = (x × y ) *~ n.
+ +
+Lemma mulrzAr n x y : x × (y *~ n ) = (x × y ) *~ n.
+ +
+Lemma mulrzl x n : n %:~R × x = x *~ n.
+ +
+Lemma mulrzr x n : x × n %:~R = x *~ n.
+ +
+Lemma mulNrNz n x : (-x ) *~ (-n ) = x *~ n.
+ +
+Lemma mulrbz x (b : bool) : x *~ b = (if b then x else 0).
+ +
+Lemma intrD m n : (m + n )%:~R = m %:~R + n %:~R :> R.
+ +
+Lemma intrM m n : (m × n )%:~R = m %:~R × n %:~R :> R.
+ +
+Lemma intmul1_is_rmorphism : rmorphism ( *~%R (1 : R )).
+Canonical intmul1_rmorphism := RMorphism intmul1_is_rmorphism.
+ +
+Lemma mulr2z n : n *~ 2 = n + n.
+ +
+End RintMod.
+ +
+Lemma mulrzz m n : m *~ n = m × n.
+ +
+Lemma mulz2 n : n × 2%:Z = n + n.
+ +
+Lemma mul2z n : 2%:Z × n = n + n.
+ +
+Section LMod.
+ +
+Variable R : ringType.
+Variable V : (lmodType R).
+ +
+Implicit Types m n : int.
+Implicit Types x y z : R.
+Implicit Types u v w : V.
+ +
+Lemma scaler_int n v : n %:~R *: v = v *~ n.
+ +
+Lemma scalerMzl a v n : (a *: v ) *~ n = (a *~ n ) *: v.
+ +
+Lemma scalerMzr a v n : (a *: v ) *~ n = a *: (v *~ n ).
+ +
+End LMod.
+ +
+Lemma mulrz_int (M : zmodType) (n : int) (x : M) : x *~ n %:~R = x *~ n.
+ +
+Section MorphTheory.
+Section Additive.
+Variables (U V : zmodType) (f : {additive U → V }).
+ +
+Lemma raddfMz n : {morph f : x / x *~ n }.
+ +
+End Additive.
+ +
+Section Multiplicative.
+ +
+Variables (R S : ringType) (f : {rmorphism R → S }).
+ +
+Lemma rmorphMz : ∀ n, {morph f : x / x *~ n }.
+ +
+Lemma rmorph_int : ∀ n, f n %:~R = n %:~R.
+ +
+End Multiplicative.
+ +
+Section Linear.
+ +
+Variable R : ringType.
+Variables (U V : lmodType R) (f : {linear U → V }).
+ +
+Lemma linearMn : ∀ n, {morph f : x / x *~ n }.
+ +
+End Linear.
+ +
+Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aV → rV }) :
+  scalable f.
+ +
+Section Zintmul1rMorph.
+ +
+Variable R : ringType.
+ +
+Lemma commrMz (x y : R) n : GRing.comm x y → GRing.comm x (y *~ n).
+ +
+Lemma commr_int (x : R) n : GRing.comm x n %:~R.
+ +
+End Zintmul1rMorph.
+ +
+Section ZintBigMorphism.
+ +
+Variable R : ringType.
+ +
+Lemma sumMz : ∀ I r (P : pred I) F,
+ (\sum_(i <- r | P i ) F i)%N%:~R = \sum_(i <- r | P i ) ((F i )%:~R ) :> R.
+ +
+Lemma prodMz : ∀ I r (P : pred I) F,
+ (\prod_(i <- r | P i ) F i)%N%:~R = \prod_(i <- r | P i ) ((F i )%:~R ) :> R.
+ +
+End ZintBigMorphism.
+ +
+Section Frobenius.
+ +
+Variable R : ringType.
+Implicit Types x y : R.
+ +
+Variable p : nat.
+Hypothesis charFp : p \in [char R ].
+ +
+ +
+Lemma Frobenius_autMz x n : (x *~ n )^f = x ^f *~ n.
+ +
+Lemma Frobenius_aut_int n : (n %:~R )^f = n %:~R.
+ +
+End Frobenius.
+ +
+Section NumMorphism.
+ +
+Section PO.
+ +
+Variables (R : numDomainType).
+ +
+Implicit Types n m : int.
+Implicit Types x y : R.
+ +
+Lemma rmorphzP (f : {rmorphism int → R }) : f =1 ( *~%R 1 ).
+ +
+

+ +

+ intmul and ler/ltr +

+Lemma ler_pmulz2r n (hn : 0 < n) : {mono *~%R ^~ n :x y / x ≤ y :> R }.
+ +
+Lemma ltr_pmulz2r n (hn : 0 < n) : {mono *~%R ^~ n : x y / x < y :> R }.
+ +
+Lemma ler_nmulz2r n (hn : n < 0) : {mono *~%R ^~ n : x y /~ x ≤ y :> R }.
+ +
+Lemma ltr_nmulz2r n (hn : n < 0) : {mono *~%R ^~ n : x y /~ x < y :> R }.
+ +
+Lemma ler_wpmulz2r n (hn : 0 ≤ n) : {homo *~%R ^~ n : x y / x ≤ y :> R }.
+ +
+Lemma ler_wnmulz2r n (hn : n ≤ 0) : {homo *~%R ^~ n : x y /~ x ≤ y :> R }.
+ +
+Lemma mulrz_ge0 x n (x0 : 0 ≤ x) (n0 : 0 ≤ n) : 0 ≤ x *~ n.
+ +
+Lemma mulrz_le0 x n (x0 : x ≤ 0) (n0 : n ≤ 0) : 0 ≤ x *~ n.
+ +
+Lemma mulrz_ge0_le0 x n (x0 : 0 ≤ x) (n0 : n ≤ 0) : x *~ n ≤ 0.
+ +
+Lemma mulrz_le0_ge0 x n (x0 : x ≤ 0) (n0 : 0 ≤ n) : x *~ n ≤ 0.
+ +
+Lemma pmulrz_lgt0 x n (n0 : 0 < n) : 0 < x *~ n = (0 < x ).
+ +
+Lemma nmulrz_lgt0 x n (n0 : n < 0) : 0 < x *~ n = (x < 0).
+ +
+Lemma pmulrz_llt0 x n (n0 : 0 < n) : x *~ n < 0 = (x < 0).
+ +
+Lemma nmulrz_llt0 x n (n0 : n < 0) : x *~ n < 0 = (0 < x ).
+ +
+Lemma pmulrz_lge0 x n (n0 : 0 < n) : 0 ≤ x *~ n = (0 ≤ x ).
+ +
+Lemma nmulrz_lge0 x n (n0 : n < 0) : 0 ≤ x *~ n = (x ≤ 0).
+ +
+Lemma pmulrz_lle0 x n (n0 : 0 < n) : x *~ n ≤ 0 = (x ≤ 0).
+ +
+Lemma nmulrz_lle0 x n (n0 : n < 0) : x *~ n ≤ 0 = (0 ≤ x ).
+ +
+Lemma ler_wpmulz2l x (hx : 0 ≤ x) : {homo *~%R x : x y / x ≤ y }.
+ +
+Lemma ler_wnmulz2l x (hx : x ≤ 0) : {homo *~%R x : x y /~ x ≤ y }.
+ +
+Lemma ler_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x ≤ y }.
+ +
+Lemma ler_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x ≤ y }.
+ +
+Lemma ltr_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y }.
+ +
+Lemma ltr_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x < y }.
+ +
+Lemma pmulrz_rgt0 x n (x0 : 0 < x) : 0 < x *~ n = (0 < n ).
+ +
+Lemma nmulrz_rgt0 x n (x0 : x < 0) : 0 < x *~ n = (n < 0).
+ +
+Lemma pmulrz_rlt0 x n (x0 : 0 < x) : x *~ n < 0 = (n < 0).
+ +
+Lemma nmulrz_rlt0 x n (x0 : x < 0) : x *~ n < 0 = (0 < n ).
+ +
+Lemma pmulrz_rge0 x n (x0 : 0 < x) : 0 ≤ x *~ n = (0 ≤ n ).
+ +
+Lemma nmulrz_rge0 x n (x0 : x < 0) : 0 ≤ x *~ n = (n ≤ 0).
+ +
+Lemma pmulrz_rle0 x n (x0 : 0 < x) : x *~ n ≤ 0 = (n ≤ 0).
+ +
+Lemma nmulrz_rle0 x n (x0 : x < 0) : x *~ n ≤ 0 = (0 ≤ n ).
+ +
+Lemma mulrIz x (hx : x != 0) : injective ( *~%R x).
+ +
+Lemma ler_int m n : (m %:~R ≤ n %:~R :> R ) = (m ≤ n ).
+ +
+Lemma ltr_int m n : (m %:~R < n %:~R :> R ) = (m < n ).
+ +
+Lemma eqr_int m n : (m %:~R == n %:~R :> R ) = (m == n ).
+ +
+Lemma ler0z n : (0 ≤ n %:~R :> R ) = (0 ≤ n ).
+ +
+Lemma ltr0z n : (0 < n %:~R :> R ) = (0 < n ).
+ +
+Lemma lerz0 n : (n %:~R ≤ 0 :> R ) = (n ≤ 0).
+ +
+Lemma ltrz0 n : (n %:~R < 0 :> R ) = (n < 0).
+ +
+Lemma ler1z (n : int) : (1 ≤ n %:~R :> R ) = (1 ≤ n ).
+ +
+Lemma ltr1z (n : int) : (1 < n %:~R :> R ) = (1 < n ).
+ +
+Lemma lerz1 n : (n %:~R ≤ 1 :> R ) = (n ≤ 1).
+ +
+Lemma ltrz1 n : (n %:~R < 1 :> R ) = (n < 1).
+ +
+Lemma intr_eq0 n : (n %:~R == 0 :> R ) = (n == 0).
+ +
+Lemma mulrz_eq0 x n : (x *~ n == 0) = ((n == 0) || (x == 0)).
+ +
+Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)).
+ +
+Lemma realz n : (n %:~R : R ) \in Num.real.
+ Hint Resolve realz.
+ +
+Definition intr_inj := @mulrIz 1 (oner_neq0 R).
+ +
+End PO.
+ +
+End NumMorphism.
+ +
+End MorphTheory.
+ +
+ +
+Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
+  match n with
+    | Posz n ⇒ x ^+ n
+    | Negz n ⇒ x ^- (n .+1 )
+  end.
+ +
+Notation "x ^ n" := (exprz x n) : ring_scope.
+ +
+Section ExprzUnitRing.
+ +
+Variable R : unitRingType.
+Implicit Types x y : R.
+Implicit Types m n : int.
+ +
+Lemma exprnP x (n : nat) : x ^+ n = x ^ n.
+ +
+Lemma exprnN x (n : nat) : x ^- n = x ^ -n %:Z.
+ +
+Lemma expr0z x : x ^ 0 = 1.
+ +
+Lemma expr1z x : x ^ 1 = x.
+ +
+Lemma exprN1 x : x ^ (-1) = x ^-1.
+ +
+Lemma invr_expz x n : (x ^ n )^-1 = x ^ (- n ).
+ +
+Lemma exprz_inv x n : (x ^-1 ) ^ n = x ^ (- n ).
+ +
+Lemma exp1rz n : 1 ^ n = 1 :> R.
+ +
+Lemma exprSz x (n : nat) : x ^ n .+1 = x × x ^ n.
+ +
+Lemma exprSzr x (n : nat) : x ^ n .+1 = x ^ n × x.
+ +
+Fact exprzD_nat x (m n : nat) : x ^ (m %:Z + n ) = x ^ m × x ^ n.
+ +
+Fact exprzD_Nnat x (m n : nat) : x ^ (-m %:Z + -n %:Z ) = x ^ (-m %:Z ) × x ^ (-n %:Z ).
+ +
+Lemma exprzD_ss x m n : (0 ≤ m ) && (0 ≤ n ) || (m ≤ 0) && (n ≤ 0)
+  → x ^ (m + n ) = x ^ m × x ^ n.
+ +
+Lemma exp0rz n : 0 ^ n = (n == 0)%:~R :> R.
+ +
+Lemma commrXz x y n : GRing.comm x y → GRing.comm x (y ^ n).
+ +
+Lemma exprMz_comm x y n : x \is a GRing.unit → y \is a GRing.unit →
+  GRing.comm x y → (x × y ) ^ n = x ^ n × y ^ n.
+ +
+Lemma commrXz_wmulls x y n :
+  0 ≤ n → GRing.comm x y → (x × y ) ^ n = x ^ n × y ^ n.
+ +
+Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit.
+ +
+Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n ) = x ^ m × x ^ n.
+ +
+Lemma exprz_exp x m n : (x ^ m ) ^ n = (x ^ (m × n )).
+ +
+Lemma exprzAC x m n : (x ^ m ) ^ n = (x ^ n ) ^ m.
+ +
+Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 ≤ n) :
+  x ^ (- n ) = x ^ n.
+ +
+End ExprzUnitRing.
+ +
+Section Exprz_Zint_UnitRing.
+ +
+Variable R : unitRingType.
+Implicit Types x y : R.
+Implicit Types m n : int.
+ +
+Lemma exprz_pmulzl x m n : 0 ≤ n → (x *~ m ) ^ n = x ^ n *~ (m ^ n ).
+ +
+Lemma exprz_pintl m n (hn : 0 ≤ n) : m %:~R ^ n = (m ^ n )%:~R :> R.
+ +
+Lemma exprzMzl x m n (ux : x \is a GRing.unit) (um : m %:~R \is a @GRing.unit R):
+   (x *~ m ) ^ n = (m %:~R ^ n ) × x ^ n :> R.
+ +
+Lemma expNrz x n : (- x ) ^ n = (-1) ^ n × x ^ n :> R.
+ +
+Lemma unitr_n0expz x n :
+  n != 0 → (x ^ n \is a GRing.unit ) = (x \is a GRing.unit ).
+ +
+Lemma intrV (n : int) :
+  n \in [:: 0; 1; -1] → n %:~R ^-1 = n %:~R :> R.
+ +
+Lemma rmorphXz (R' : unitRingType) (f : {rmorphism R → R'}) n :
+  {in GRing.unit , {morph f : x / x ^ n }}.
+ +
+End Exprz_Zint_UnitRing.
+ +
+Section ExprzIdomain.
+ +
+Variable R : idomainType.
+Implicit Types x y : R.
+Implicit Types m n : int.
+ +
+Lemma expfz_eq0 x n : (x ^ n == 0) = (n != 0) && (x == 0).
+ +
+Lemma expfz_neq0 x n : x != 0 → x ^ n != 0.
+ +
+Lemma exprzMl x y n (ux : x \is a GRing.unit) (uy : y \is a GRing.unit) :
+  (x × y ) ^ n = x ^ n × y ^ n.
+ +
+Lemma expfV (x : R) (i : int) : (x ^ i ) ^-1 = (x ^-1 ) ^ i.
+ +
+End ExprzIdomain.
+ +
+Section ExprzField.
+ +
+Variable F : fieldType.
+Implicit Types x y : F.
+Implicit Types m n : int.
+ +
+Lemma expfzDr x m n : x != 0 → x ^ (m + n ) = x ^ m × x ^ n.
+ +
+Lemma expfz_n0addr x m n : m + n != 0 → x ^ (m + n ) = x ^ m × x ^ n.
+ +
+Lemma expfzMl x y n : (x × y ) ^ n = x ^ n × y ^ n.
+ +
+Lemma fmorphXz (R : unitRingType) (f : {rmorphism F → R }) n :
+  {morph f : x / x ^ n }.
+ +
+End ExprzField.
+ +
+Section ExprzOrder.
+ +
+Variable R : realFieldType.
+Implicit Types x y : R.
+Implicit Types m n : int.
+ +
+

+ +

+ ler and exprz +

+Lemma exprz_ge0 n x (hx : 0 ≤ x) : (0 ≤ x ^ n).
+ +
+Lemma exprz_gt0 n x (hx : 0 < x) : (0 < x ^ n).
+ +
+Definition exprz_gte0 := (exprz_ge0 , exprz_gt0 ).
+ +
+Lemma ler_wpiexpz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
+  {in ≥ 0 &, {homo (exprz x ) : x y /~ x ≤ y }}.
+ +
+Lemma ler_wniexpz2l x (x0 : 0 ≤ x) (x1 : x ≤ 1) :
+  {in < 0 &, {homo (exprz x ) : x y /~ x ≤ y }}.
+ +
+Fact ler_wpeexpz2l x (x1 : 1 ≤ x) :
+  {in ≥ 0 &, {homo (exprz x ) : x y / x ≤ y }}.
+ +
+Fact ler_wneexpz2l x (x1 : 1 ≤ x) :
+  {in ≤ 0 &, {homo (exprz x ) : x y / x ≤ y }}.
+ +
+Lemma ler_weexpz2l x (x1 : 1 ≤ x) : {homo (exprz x ) : x y / x ≤ y }.
+ +
+Lemma pexprz_eq1 x n (x0 : 0 ≤ x) : (x ^ n == 1) = ((n == 0) || (x == 1)).
+ +
+Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x).
+ +
+Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
+  {in ≥ 0 &, {mono (exprz x ) : x y /~ x ≤ y }}.
+ +
+Lemma ltr_piexpz2l x (x0 : 0 < x) (x1 : x < 1) :
+  {in ≥ 0 &, {mono (exprz x ) : x y /~ x < y }}.
+ +
+Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
+  {in < 0 &, {mono (exprz x ) : x y /~ x ≤ y }}.
+ +
+Lemma ltr_niexpz2l x (x0 : 0 < x) (x1 : x < 1) :
+  {in < 0 &, {mono (exprz x ) : x y /~ x < y }}.
+ +
+Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x ) : x y / x ≤ y }.
+ +
+Lemma ltr_eexpz2l x (x1 : 1 < x) : {mono (exprz x ) : x y / x < y }.
+ +
+Lemma ler_wpexpz2r n (hn : 0 ≤ n) :
+{in ≥ 0 & , {homo ((@exprz R )^~ n ) : x y / x ≤ y }}.
+ +
+Lemma ler_wnexpz2r n (hn : n ≤ 0) :
+{in > 0 & , {homo ((@exprz R )^~ n ) : x y /~ x ≤ y }}.
+ +
+Lemma pexpIrz n (n0 : n != 0) : {in ≥ 0 &, injective ((@exprz R )^~ n)}.
+ +
+Lemma nexpIrz n (n0 : n != 0) : {in ≤ 0 &, injective ((@exprz R )^~ n)}.
+ +
+Lemma ler_pexpz2r n (hn : 0 < n) :
+  {in ≥ 0 & , {mono ((@exprz R )^~ n ) : x y / x ≤ y }}.
+ +
+Lemma ltr_pexpz2r n (hn : 0 < n) :
+  {in ≥ 0 & , {mono ((@exprz R )^~ n ) : x y / x < y }}.
+ +
+Lemma ler_nexpz2r n (hn : n < 0) :
+  {in > 0 & , {mono ((@exprz R )^~ n ) : x y /~ x ≤ y }}.
+ +
+Lemma ltr_nexpz2r n (hn : n < 0) :
+  {in > 0 & , {mono ((@exprz R )^~ n ) : x y /~ x < y }}.
+ +
+Lemma eqr_expz2 n x y : n != 0 → 0 ≤ x → 0 ≤ y →
+  (x ^ n == y ^ n ) = (x == y ).
+ +
+End ExprzOrder.
+ +
+ +
+Section Sgz.
+ +
+Variable R : numDomainType.
+Implicit Types x y z : R.
+Implicit Types m n p : int.
+ +
+Definition sgz x : int := if x == 0 then 0 else if x < 0 then -1 else 1.
+ +
+Lemma sgz_def x : sgz x = (-1) ^+ (x < 0)%R *+ (x != 0).
+ +
+Lemma sgrEz x : sgr x = (sgz x )%:~R.
+ +
+Lemma gtr0_sgz x : 0 < x → sgz x = 1.
+ +
+Lemma ltr0_sgz x : x < 0 → sgz x = -1.
+ +
+Lemma sgz0 : sgz (0 : R) = 0.
+Lemma sgz1 : sgz (1 : R) = 1.
+Lemma sgzN1 : sgz (-1 : R) = -1.
+ +
+Definition sgzE := (sgz0 , sgz1 , sgzN1 ).
+ +
+Lemma sgz_sgr x : sgz (sgr x) = sgz x.
+ +
+Lemma normr_sgz x : `|sgz x | = (x != 0).
+ +
+Lemma normr_sg x : `|sgr x | = (x != 0)%:~R.
+ +
+End Sgz.
+ +
+Section MoreSgz.
+ +
+Variable R : numDomainType.
+ +
+Lemma sgz_int m : sgz (m %:~R : R) = sgz m.
+ +
+Lemma sgrz (n : int) : sgr n = sgz n.
+ +
+Lemma intr_sg m : (sgr m )%:~R = sgr (m %:~R) :> R.
+ +
+Lemma sgz_id (x : R) : sgz (sgz x) = sgz x.
+ +
+End MoreSgz.
+ +
+Section SgzReal.
+ +
+Variable R : realDomainType.
+Implicit Types x y z : R.
+Implicit Types m n p : int.
+ +
+Lemma sgz_cp0 x :
+  ((sgz x == 1) = (0 < x )) ×
+  ((sgz x == -1) = (x < 0)) ×
+  ((sgz x == 0) = (x == 0)).
+ +
+CoInductive sgz_val x : bool → bool → bool → bool → bool → bool
+  → bool → bool → bool → bool → bool → bool
+  → bool → bool → bool → bool → bool → bool
+  → R → R → int → Set :=
+  | SgzNull of x = 0 : sgz_val x true true true true false false
+    true false false true false false true false false true false false 0 0 0
+  | SgzPos of x > 0 : sgz_val x false false true false false true
+    false false true false false true false false true false false true x 1 1
+  | SgzNeg of x < 0 : sgz_val x false true false false true false
+    false true false false true false false true false false true false (-x) (-1) (-1).
+ +
+Lemma sgzP x :
+  sgz_val x (0 == x) (x ≤ 0) (0 ≤ x) (x == 0) (x < 0) (0 < x)
+  (0 == sgr x) (-1 == sgr x) (1 == sgr x)
+  (sgr x == 0) (sgr x == -1) (sgr x == 1)
+  (0 == sgz x) (-1 == sgz x) (1 == sgz x)
+  (sgz x == 0) (sgz x == -1) (sgz x == 1) `|x | (sgr x) (sgz x).
+ +
+Lemma sgzN x : sgz (- x) = - sgz x.
+ +
+Lemma mulz_sg x : sgz x × sgz x = (x != 0)%:~R.
+ +
+Lemma mulz_sg_eq1 x y : (sgz x × sgz y == 1) = (x != 0) && (sgz x == sgz y ).
+ +
+Lemma mulz_sg_eqN1 x y : (sgz x × sgz y == -1) = (x != 0) && (sgz x == - sgz y ).
+ +
+

+ +

+ Lemma muls_eqA x y z : sgr x != 0 -> + (sgr y * sgr z == sgr x) = ((sgr y * sgr x == sgr z) && (sgr z != 0)). + Proof. by do 3!case: sgrP=> _. Qed. +

+ +
+Lemma sgzM x y : sgz (x × y) = sgz x × sgz y.
+ +
+Lemma sgzX (n : nat) x : sgz (x ^+ n) = (sgz x ) ^+ n.
+ +
+Lemma sgz_eq0 x : (sgz x == 0) = (x == 0).
+ +
+Lemma sgz_odd (n : nat) x : x != 0 → (sgz x ) ^+ n = (sgz x ) ^+ (odd n ).
+ +
+Lemma sgz_gt0 x : (sgz x > 0) = (x > 0).
+ +
+Lemma sgz_lt0 x : (sgz x < 0) = (x < 0).
+ +
+Lemma sgz_ge0 x : (sgz x ≥ 0) = (x ≥ 0).
+ +
+Lemma sgz_le0 x : (sgz x ≤ 0) = (x ≤ 0).
+ +
+Lemma sgz_smul x y : sgz (y *~ (sgz x )) = (sgz x ) × (sgz y ).
+ +
+Lemma sgrMz m x : sgr (x *~ m) = sgr x *~ sgr m.
+ +
+End SgzReal.
+ +
+Lemma sgz_eq (R R' : realDomainType) (x : R) (y : R') :
+  (sgz x == sgz y ) = ((x == 0) == (y == 0)) && ((0 < x ) == (0 < y )).
+ +
+Lemma intr_sign (R : ringType) s : ((-1) ^+ s )%:~R = (-1) ^+ s :> R.
+ +
+Section Absz.
+ +
+Implicit Types m n p : int.
+Open Scope nat_scope.
+ +
+Lemma absz_nat (n : nat) : `|n | = n.
+ +
+Lemma abszE (m : int) : `|m | = `|m |%R :> int.
+ +
+Lemma absz0 : `|0%R| = 0.
+ +
+Lemma abszN m : `|- m | = `|m |.
+ +
+Lemma absz_eq0 m : (`|m | == 0) = (m == 0%R).
+ +
+Lemma absz_gt0 m : (`|m | > 0) = (m != 0%R).
+ +
+Lemma absz1 : `|1%R| = 1.
+ +
+Lemma abszN1 : `|-1%R| = 1.
+ +
+Lemma absz_id m : `|(`|m |)| = `|m |.
+ +
+Lemma abszM m1 m2 : `|(m1 × m2)%R| = `|m1 | × `|m2 |.
+ +
+Lemma abszX (n : nat) m : `|m ^+ n | = `|m | ^ n.
+ +
+Lemma absz_sg m : `|sgr m | = (m != 0%R).
+ +
+Lemma gez0_abs m : (0 ≤ m)%R → `|m | = m :> int.
+ +
+Lemma gtz0_abs m : (0 < m)%R → `|m | = m :> int.
+ +
+Lemma lez0_abs m : (m ≤ 0)%R → `|m | = - m :> int.
+ +
+Lemma ltz0_abs m : (m < 0)%R → `|m | = - m :> int.
+ +
+Lemma absz_sign s : `|(-1) ^+ s | = 1.
+ +
+Lemma abszMsign s m : `|((-1) ^+ s × m)%R| = `|m |.
+ +
+Lemma mulz_sign_abs m : ((-1) ^+ (m < 0)%R × `|m |%:Z)%R = m.
+ +
+Lemma mulz_Nsign_abs m : ((-1) ^+ (0 < m)%R × `|m |%:Z)%R = - m.
+ +
+Lemma intEsign m : m = ((-1) ^+ (m < 0)%R × `|m |%:Z)%R.
+ +
+Lemma abszEsign m : `|m |%:Z = ((-1) ^+ (m < 0)%R × m)%R.
+ +
+Lemma intEsg m : m = (sgz m × `|m |%:Z)%R.
+ +
+Lemma abszEsg m : (`|m |%:Z = sgz m × m)%R.
+ +
+End Absz.
+ +
+Module Export IntDist.
+ +
+Notation "m - n" :=
+  (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
+Notation "`| m |" := (absz m) : nat_scope.
+Coercion Posz : nat >-> int.
+ +
+Section Distn.
+ +
+Open Scope nat_scope.
+Implicit Type m : int.
+Implicit Types n d : nat.
+ +
+Lemma distnC m1 m2 : `|m1 - m2 | = `|m2 - m1 |.
+ +
+Lemma distnDl d n1 n2 : `|d + n1 - (d + n2 )| = `|n1 - n2 |.
+ +
+Lemma distnDr d n1 n2 : `|n1 + d - (n2 + d )| = `|n1 - n2 |.
+ +
+Lemma distnEr n1 n2 : n1 ≤ n2 → `|n1 - n2 | = n2 - n1.
+ +
+Lemma distnEl n1 n2 : n2 ≤ n1 → `|n1 - n2 | = n1 - n2.
+ +
+Lemma distn0 n : `|n - 0| = n.
+ +
+Lemma dist0n n : `|0 - n | = n.
+ +
+Lemma distnn m : `|m - m | = 0.
+ +
+Lemma distn_eq0 n1 n2 : (`|n1 - n2 | == 0) = (n1 == n2 ).
+ +
+Lemma distnS n : `|n - n .+1 | = 1.
+ +
+Lemma distSn n : `|n .+1 - n | = 1.
+ +
+Lemma distn_eq1 n1 n2 :
+  (`|n1 - n2 | == 1) = (if n1 < n2 then n1 .+1 == n2 else n1 == n2 .+1 ).
+ +
+Lemma leq_add_dist m1 m2 m3 : `|m1 - m3 | ≤ `|m1 - m2 | + `|m2 - m3 |.
+ +
+

+ +

+ Most of this proof generalizes to all real-ordered rings. +

+Lemma leqif_add_distz m1 m2 m3 :
+  `|m1 - m3 | ≤ `|m1 - m2 | + `|m2 - m3 |
+             ?= iff (m1 ≤ m2 ≤ m3)%R || (m3 ≤ m2 ≤ m1)%R.
+ +
+Lemma leqif_add_dist n1 n2 n3 :
+  `|n1 - n3 | ≤ `|n1 - n2 | + `|n2 - n3 |
+             ?= iff (n1 ≤ n2 ≤ n3 ) || (n3 ≤ n2 ≤ n1 ).
+ +
+Lemma sqrn_dist n1 n2 : `|n1 - n2 | ^ 2 + 2 × (n1 × n2 ) = n1 ^ 2 + n2 ^ 2.
+ +
+End Distn.
+ +
+End IntDist.
+ +
+Section NormInt.
+ +
+Variable R : numDomainType.
+ +
+Lemma intr_norm m : `|m |%:~R = `|m %:~R | :> R.
+ +
+Lemma normrMz m (x : R) : `|x *~ m | = `|x | *~ `|m |.
+ +
+Lemma expN1r (i : int) : (-1 : R ) ^ i = (-1) ^+ `|i |.
+ +
+End NormInt.
+ +
+Section PolyZintRing.
+ +
+Variable R : ringType.
+Implicit Types x y z: R.
+Implicit Types m n : int.
+Implicit Types i j k : nat.
+Implicit Types p q r : {poly R }.
+ +
+Lemma coefMrz : ∀ p n i, (p *~ n )`_i = (p `_i *~ n ).
+ +
+Lemma polyC_mulrz : ∀ n, {morph (@polyC R ) : c / c *~ n }.
+ +
+Lemma hornerMz : ∀ n (p : {poly R }) x, (p *~ n ).[x ] = p .[x ] *~ n.
+ +
+Lemma horner_int : ∀ n x, (n %:~R : {poly R }).[x ] = n %:~R.
+ +
+Lemma derivMz : ∀ n p, (p *~ n )^` = p ^` *~ n.
+ +
+End PolyZintRing.
+ +
+Section PolyZintOIdom.
+ +
+Variable R : realDomainType.
+ +
+Lemma mulpz (p : {poly R }) (n : int) : p *~ n = n %:~R *: p.
+ +
+End PolyZintOIdom.
+ +
+Section ZnatPred.
+ +
+Definition Znat := [qualify a n : int | 0 ≤ n ].
+Fact Znat_key : pred_key Znat.
+Canonical Znat_keyd := KeyedQualifier Znat_key.
+ +
+Lemma Znat_def n : (n \is a Znat ) = (0 ≤ n ).
+ +
+Lemma Znat_semiring_closed : semiring_closed Znat.
+ Canonical Znat_addrPred := AddrPred Znat_semiring_closed.
+Canonical Znat_mulrPred := MulrPred Znat_semiring_closed.
+Canonical Znat_semiringPred := SemiringPred Znat_semiring_closed.
+ +
+Lemma ZnatP (m : int) : reflect (∃ n : nat , m = n) (m \is a Znat).
+ +
+End ZnatPred.
+ +
+Section rpred.
+ +
+Lemma rpredMz M S (addS : @zmodPred M S) (kS : keyed_pred addS) m :
+  {in kS , ∀ u, u *~ m \in kS }.
+ +
+Lemma rpred_int R S (ringS : @subringPred R S) (kS : keyed_pred ringS) m :
+  m %:~R \in kS.
+ +
+Lemma rpredZint (R : ringType) (M : lmodType R) S
+                 (addS : @zmodPred M S) (kS : keyed_pred addS) m :
+  {in kS , ∀ u, m %:~R *: u \in kS }.
+ +
+Lemma rpredXz R S (divS : @divrPred R S) (kS : keyed_pred divS) m :
+  {in kS , ∀ x, x ^ m \in kS }.
+ +
+Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x :
+  (x ^ ((-1) ^+ n ) \in kS ) = (x \in kS ).
+ +
+End rpred.
+