Library mathcomp.algebra.ssrint

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

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
From mathcomp Require Import fintype finfun bigop order ssralg countalg ssrnum.
From mathcomp Require Import poly.

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. <number> == <number> as an int, with <number> an optional minus sign followed by a sequence of digits. This notation is in int_scope (delimited with %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.

Declare Scope int_scope.
Declare Scope distn_scope.
Declare Scope rat_scope.

Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").
Reserved Notation "n = m :> 'int'"
(at level 70, m at next level, format "n = m :> 'int'").
Reserved Notation "n == m :> 'int'"
(at level 70, m at next level, format "n == m :> 'int'").
Reserved Notation "n != m :> 'int'"
(at level 70, m at next level, format "n != m :> 'int'").
Reserved Notation "n <> m :> 'int'"
(at level 70, m at next level, format "n <> m :> 'int'").

Import Order.TTheory 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) (only parsing) : int_scope.
Notation "n %:Z" := (Posz n) (only parsing) : ring_scope.

Notation "n = m :> 'int'" := (@eq int n%Z m%Z) (only parsing) : ring_scope.
Notation "n = m :> 'int'" := (Posz n = Posz m) (only printing) : ring_scope.
Notation "n == m :> 'int'" := ((n%Z : int) == (m%Z : int)) (only parsing)
: ring_scope.
Notation "n == m :> 'int'" := (Posz n == Posz m) (only printing) : ring_scope.
Notation "n != m :> 'int'" := ((n%Z : int) != (m%Z : int)) (only parsing)
: ring_scope.
Notation "n != m :> 'int'" := (Posz n != Posz m) (only printing) : ring_scope.
Notation "n <> m :> 'int'" := (not (@eq int n%Z m%Z)) (only parsing)
: ring_scope.
Notation "n <> m :> 'int'" := (Posz n Posz m) (only printing) : ring_scope.

Definition parse_int (x : Number.int) : int :=
match x with
| Number.IntDecimal (Decimal.Pos u) ⇒ Posz (Nat.of_uint u)
| Number.IntDecimal (Decimal.Neg u) ⇒ Negz (Nat.of_uint u).-1
end.

Definition print_int (x : int) : Number.int :=
match x with
| Posz nNumber.IntDecimal (Decimal.Pos (Nat.to_uint n))
| Negz nNumber.IntDecimal (Decimal.Neg (Nat.to_uint n.+1))
end.

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.

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.

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 oppzK : involutive oppz.

Lemma oppzD : {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 predn_int (n : nat) : 0 < n n.-1%:Z = n - 1.

End intZmod.
End intZmod.

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 oppzD := @opprD 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 := GRing.Zmodule_isComRing.Build int

End intRing.
End intRing.

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

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 := GRing.ComRing_hasMulInverse.Build int
mulVz unitzPl invz_out.

End intUnitRing.
End intUnitRing.

Definition absz m := match m with Posz pp | Negz nn.+1 end.
Notation "m - n" := (@GRing.add int m%N (@GRing.opp int n%N)) : distn_scope.
Arguments absz m%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_add m n : lez 0 m lez 0 n lez 0 (m + n).

Fact lez_mul m n : lez 0 m lez 0 n lez 0 (m × n).

Fact lez_anti m : lez 0 m lez m 0 m = 0.

Lemma subz_ge0 m n : lez 0 (n - m) = lez m n.

Fact lez_total m n : lez m n || lez n m.

Fact normzN m : normz (- m) = normz m.

Fact gez0_norm m : lez 0 m normz m = m.

Fact ltz_def m n : (ltz m n) = (n != m) && (lez m n).

Definition Mixin := Num.IntegralDomain_isLeReal.Build int
lez_add lez_mul lez_anti subz_ge0 (lez_total 0) normzN gez0_norm ltz_def.

End intOrdered.
End intOrdered.

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 != 0).

Definition lteNz_nat := (leNz_nat, ltNz_nat).

Lemma lezN_nat m n : (m%:Z - n%:Z) = (m == 0) && (n == 0).

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 :> 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 lez1D x y : (1 + x y) = (x < y).

Lemma lezD1 x y : (x + 1 y) = (x < y).

Lemma ltz1D x y : (x < 1 + y) = (x y).

Lemma ltzD1 x y : (x < y + 1) = (x y).

End intOrderedTheory.

Bind Scope ring_scope with int.

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") : function_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 mulrzDl_tmp 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 mulrzDr_tmp x : {morph *~%R x : m n / m + n}.

(* FIXME, the error message below "nomsg" when we forget this line is not very helpful *)

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.

End ZintLmod.

#[deprecated(since="mathcomp 2.1.0", note="Use mulrzDr_tmp instead. mulrzDl will be renamed mulrzDr in the future.")]
Notation mulrzDl := mulrzDr_tmp.
#[deprecated(since="mathcomp 2.1.0", note="Use mulrzDl_tmp instead. mulrzDr will be renamed mulrzDl in the future.")]
Notation mulrzDr := mulrzDl_tmp.

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_multiplicative : multiplicative ( *~%R (1 : R)).

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.
Variables (U V : zmodType) (f : {additive U V}).

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

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_pMz2r n (hn : 0 < n) : {mono *~%R^~ n :x y / x y :> R}.

Lemma ltr_pMz2r n (hn : 0 < n) : {mono *~%R^~ n : x y / x < y :> R}.

Lemma ler_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x y :> R}.

Lemma ltr_nMz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x < y :> R}.

Lemma ler_wpMz2r n (hn : 0 n) : {homo *~%R^~ n : x y / x y :> R}.

Lemma ler_wnMz2r 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_wpMz2l x (hx : 0 x) : {homo *~%R x : x y / x y}.

Lemma ler_wnMz2l x (hx : x 0) : {homo *~%R x : x y /~ x y}.

Lemma ler_pMz2l x (hx : 0 < x) : {mono *~%R x : x y / x y}.

Lemma ler_nMz2l x (hx : x < 0) : {mono *~%R x : x y /~ x y}.

Lemma ltr_pMz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y}.

Lemma ltr_nMz2l 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.
Notation ler_pmulz2r := ler_pMz2r.
Notation ler_pmulz2l := ler_pMz2l.
Notation ler_wpmulz2r := ler_wpMz2r.
Notation ler_wpmulz2l := ler_wpMz2l.
Notation ler_wnmulz2l := ler_wnMz2l.
Notation ler_nmulz2r := ler_nMz2r.
Notation ler_nmulz2l := ler_nMz2l.
Notation ltr_pmulz2r := ltr_pMz2r.
Notation ltr_pmulz2l := ltr_pMz2l.
Notation ltr_nmulz2r := ltr_nMz2r.
Notation ltr_nmulz2l := ltr_nMz2l.

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.

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_pMzl 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_wpiXz2l x (x0 : 0 x) (x1 : x 1) :
{in 0 &, {homo exprz x : x y /~ x y}}.

Lemma ler_wniXz2l x (x0 : 0 x) (x1 : x 1) :
{in < 0 &, {homo exprz x : x y /~ x y}}.

Fact ler_wpeXz2l x (x1 : 1 x) : {in 0 &, {homo exprz x : x y / x y}}.

Fact ler_wneXz2l x (x1 : 1 x) : {in 0 &, {homo exprz x : x y / x y}}.

Lemma ler_weXz2l 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_piXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in 0 &, {mono exprz x : x y /~ x y}}.

Lemma ltr_piXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in 0 &, {mono exprz x : x y /~ x < y}}.

Lemma ler_niXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono exprz x : x y /~ x y}}.

Lemma ltr_niXz2l x (x0 : 0 < x) (x1 : x < 1) :
{in < 0 &, {mono (exprz x) : x y /~ x < y}}.

Lemma ler_eXz2l x (x1 : 1 < x) : {mono exprz x : x y / x y}.

Lemma ltr_eXz2l x (x1 : 1 < x) : {mono exprz x : x y / x < y}.

Lemma ler_wpXz2r n (hn : 0 n) :
{in 0 & , {homo (@exprz R)^~ n : x y / x y}}.

Lemma ler_wnXz2r 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_pXz2r n (hn : 0 < n) :
{in 0 & , {mono ((@exprz R)^~ n) : x y / x y}}.

Lemma ltr_pXz2r n (hn : 0 < n) :
{in 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}.

Lemma ler_nXz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x y}}.

Lemma ltr_nXz2r n (hn : n < 0) :
{in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}.

Lemma eqrXz2 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.
Notation ler_wnmulz2r := ler_wnMz2r.
Notation ler_wpexpz2r := ler_wpXz2r.
Notation ler_wnexpz2r := ler_wnXz2r.
Notation ler_pexpz2r := ler_pXz2r.
Notation ltr_pexpz2r := ltr_pXz2r.
Notation ler_nexpz2r := ler_nXz2r.
Notation ltr_nexpz2r := ltr_nXz2r.
Notation ler_wpiexpz2l := ler_wpiXz2l.
Notation ler_wniexpz2l := ler_wniXz2l.
Notation ler_wpeexpz2l := ler_wpeXz2l.
Notation ler_wneexpz2l := ler_wneXz2l.
Notation ler_weexpz2l := ler_weXz2l.
Notation ler_piexpz2l := ler_piXz2l.
Notation ltr_piexpz2l := ltr_piXz2l.
Notation ler_niexpz2l := ler_niXz2l.
Notation ltr_niexpz2l := ltr_niXz2l.
Notation ler_eexpz2l := ler_eXz2l.
Notation ltr_eexpz2l := ltr_eXz2l.
Notation eqr_expz2 := eqrXz2.
Notation exprz_pmulzl := exprz_pMzl.

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 lez_abs m : m `|m|%N :> 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.

Section MoreAbsz.
Variable R : numDomainType.
Implicit Type i : int.

Lemma mulr_absz (x : R) i : x *+ `|i| = x *~ `|i|.

Lemma natr_absz i : `|i|%:R = `|i|%:~R :> R.

End MoreAbsz.

Module Export IntDist.

This notation is supposed to work even if the ssrint library is not Imported. Since we can't rely on the CS database to contain the zmodule instance on int we put the instance by hand in the notation.
Notation "m - n" :=
(@GRing.opp int_zmodType (n%N : int))) : distn_scope.
Arguments absz m%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 leqD_dist m1 m2 m3 : `|m1 - m3| `|m1 - m2| + `|m2 - m3|.

Most of this proof generalizes to all real-ordered rings.
Lemma leqifD_distz m1 m2 m3 :
`|m1 - m3| `|m1 - m2| + `|m2 - m3|
?= iff (m1 m2 m3)%R || (m3 m2 m1)%R.

Lemma leqifD_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 polyCMz n : {morph (@polyC R) : c / c *~ n}.

Lemma hornerMz n p 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.

Lemma mulpz p n : p *~ n = n%:~R *: p.

End PolyZintRing.

Module intArchimedean.
Section intArchimedean.

Implicit Types n : int.

Let trunc n : nat := if n is Posz n' then n' else 0%N.

Lemma truncP n :
if 0 n then (trunc n)%:R n < (trunc n).+1%:R else trunc n == 0%N.

Lemma is_natE n : (0 n) = ((trunc n)%:R == n).

Lemma is_intE n : true = (0 n) || (0 - n).

End intArchimedean.
End intArchimedean.

Section rpred.

Lemma rpredMz (M : zmodType) (S : zmodClosed M) m :
{in S, u, u *~ m \in S}.

Lemma rpred_int (R : ringType) (S : subringClosed R) m : m%:~R \in S.

Lemma rpredZint (R : ringType) (M : lmodType R) (S : zmodClosed M) m :
{in S, u, m%:~R *: u \in S}.

Lemma rpredXz (R : unitRingType) (S : divClosed R) m :
{in S, x, x ^ m \in S}.

Lemma rpredXsign (R : unitRingType) (S : divClosed R) n x :
(x ^ ((-1) ^+ n) \in S) = (x \in S).

End rpred.

Module mc_2_0.

End mc_2_0.