- -

Library mathcomp.algebra.ssrint

- -

-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
- Distributed under the terms of CeCILL-B. *)
- -
-

- -

- 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.
- -
-Import GRing.Theory Num.Theory.
-Delimit Scope int_scope with Z.
-Local Open Scope int_scope.
- -
-

- -

- Defining int -

-Variant 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.
- -
-Variant 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.
- -
-Variant 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.
- -
-Canonical int_countZmodType := [countZmodType of int ].
-Canonical int_countRingType := [countRingType of int ].
-Canonical int_countComRingType := [countComRingType of int ].
-Canonical int_countUnitRingType := [countUnitRingType of int ].
-Canonical int_countComUnitRingType := [countComUnitRingType of int ].
-Canonical int_countIdomainType := [countIdomainType of int ].
- -
-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 : core.
- -
-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)).
- -
-Variant 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.
-