(Joint Center)Library MathComp.ssrint

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
Require Import fintype finfun bigop ssralg ssrnum poly.
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 pinl _ p | Negz ninr _ n end.

Definition int_of_natsum (m : nat + nat) :=
  match m with inl pPosz p | inr nNegz 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 nif n is (n'.+1)%N then Negz n' else Posz 0
    | Negz nPosz (n.+1)%N
  end.

Local Notation "0" := (Posz 0) : int_scope.
Local Notation "-%Z" := (@oppz) : int_scope.
Local Notation "- x" := (oppz x) : int_scope.
Local Notation "+%Z" := (@addz) : int_scope.
Local Notation "x + y" := (addz x y) : int_scope.
Local Notation "x - y" := (x + - y) : int_scope.

Lemma PoszD : {morph Posz : m n / (m + n)%N >-> m + n}.

Local Coercion Posz : nat >-> int.

Lemma NegzE (n : nat) : Negz n = - n.+1.

Lemma int_rect (P : intType) :
  P 0 → ( n : nat, P nP (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) : intType :=
| 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 < nn.-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.

Local Coercion Posz : nat >-> int.

Lemma PoszD : {morph Posz : n m / (n + m)%N >-> n + m}.

Lemma NegzE (n : nat) : Negz n = -(n.+1)%:Z.

Lemma int_rect (P : intType) :
  P 0 → ( n : nat, P nP (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) : intType :=
| 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)%Nm%: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.

Local Coercion Posz : nat >-> int.

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.

Local Notation "1" := (1%N:int) : int_scope.
Local Notation "*%Z" := (@mulz) : int_scope.
Local Notation "x * y" := (mulz x y) : int_scope.

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.
Local Coercion Posz : nat >-> 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)%Nn.-1%:Z = n%:Z - 1.

End intRingTheory.

Module intUnitRing.
Section intUnitRing.
Implicit Types m n : int.
Local Coercion Posz : nat >-> 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 pp | Negz nn.+1 end.
Notation "m - n" :=
  (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope.
Local Notation "`| m |" := (absz m) : nat_scope.

Module intOrdered.
Section intOrdered.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> int.

Local Notation normz m := (absz m)%:Z.

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 xltz 0 yltz 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 nnormz 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.

Local Coercion Posz : nat >-> int.
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.
Local Notation "M ^z" := (zmodule M) (at level 2, format "M ^z") : type_scope.
Local Coercion Posz : nat >-> int.

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 : MM) : 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 xx *~ 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 : IM),
  (\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 IM}) 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.

Local Coercion Posz : nat >-> int.
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).
Local Coercion Posz : nat >-> int.

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.
Local Coercion Posz : nat >-> int.
Section Additive.
Variables (U V : zmodType) (f : {additive UV}).

Lemma raddfMz n : {morph f : x / x *~ n}.

End Additive.

Section Multiplicative.

Variables (R S : ringType) (f : {rmorphism RS}).

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 UV}).

Lemma linearMn : n, {morph f : x / x *~ n}.

End Linear.

Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aVrV}) :
  scalable f.

Section Zintmul1rMorph.

Variable R : ringType.

Lemma commrMz (x y : R) n : GRing.comm x yGRing.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].

Local Notation "x ^f" := (Frobenius_aut charFp x).

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 intR}) : 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.

Implicit Arguments intr_inj [[R] x1 x2].

Definition exprz (R : unitRingType) (x : R) (n : int) := nosimpl
  match n with
    | Posz nx ^+ n
    | Negz nx ^- (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.
Local Coercion Posz : nat >-> 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 yGRing.comm x (y ^ n).

Lemma exprMz_comm x y n : x \is a GRing.unity \is a GRing.unit
  GRing.comm x y(x × y) ^ n = x ^ n × y ^ n.

Lemma commrXz_wmulls x y n :
  0 nGRing.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.
Local Coercion Posz : nat >-> 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 RR'}) 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.
Local Coercion Posz : nat >-> 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.
Local Coercion Posz : nat >-> 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 FR}) n :
  {morph f : x / x ^ n}.

End ExprzField.

Section ExprzOrder.

Variable R : realFieldType.
Implicit Types x y : R.
Implicit Types m n : int.
Local Coercion Posz : nat >-> 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.

Local Notation sgr := Num.sg.

Section Sgz.

Variable R : numDomainType.
Implicit Types x y z : R.
Implicit Types m n p : int.
Local Coercion Posz : nat >-> 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 < xsgz 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.
Local Coercion Posz : nat >-> int.

Lemma sgz_cp0 x :
  ((sgz x == 1) = (0 < x)) ×
  ((sgz x == -1) = (x < 0)) ×
  ((sgz x == 0) = (x == 0)).

CoInductive sgz_val x : boolboolboolboolboolbool
  → boolboolboolboolboolbool
  → boolboolboolboolboolbool
  → RRintSet :=
  | 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.
Local Coercion Posz : nat >-> int.

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.