diff options
Diffstat (limited to 'mathcomp/algebra/ssrint.v')
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 1782 |
1 files changed, 1782 insertions, 0 deletions
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v new file mode 100644 index 0000000..cbf726e --- /dev/null +++ b/mathcomp/algebra/ssrint.v @@ -0,0 +1,1782 @@ +(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) +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. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Delimit Scope int_scope with Z. +Local Open Scope int_scope. + +(* Defining int *) +CoInductive int : Set := Posz of nat | Negz of nat. +(* This must be deferred to module DistInt to work around the design flaws of *) +(* the Coq module system. *) +(* Coercion Posz : nat >-> int. *) + +Notation "n %:Z" := (Posz n) + (at level 2, left associativity, format "n %:Z", only parsing) : int_scope. +Notation "n %:Z" := (Posz n) + (at level 2, left associativity, format "n %:Z", only parsing) : ring_scope. + +Notation "n = m :> 'in' 't'" := (Posz n = Posz m) + (at level 70, m at next level, format "n = m :> 'in' 't'") : ring_scope. +Notation "n == m :> 'in' 't'" := (Posz n == Posz m) + (at level 70, m at next level, format "n == m :> 'in' 't'") : ring_scope. +Notation "n != m :> 'in' 't'" := (Posz n != Posz m) + (at level 70, m at next level, format "n != m :> 'in' 't'") : ring_scope. +Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m) + (at level 70, m at next level, format "n <> m :> 'in' 't'") : ring_scope. + +Definition natsum_of_int (m : int) : nat + nat := + match m with Posz p => inl _ p | Negz n => inr _ n end. + +Definition int_of_natsum (m : nat + nat) := + match m with inl p => Posz p | inr n => Negz n end. + +Lemma natsum_of_intK : cancel natsum_of_int int_of_natsum. +Proof. by case. Qed. + +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). Proof. by []. Qed. + +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. + +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}. Proof. by []. Qed. + +Local Coercion Posz : nat >-> int. + +Lemma NegzE (n : nat) : Negz n = - n.+1. Proof. by []. Qed. + +Lemma int_rect (P : int -> Type) : + P 0 -> (forall n : nat, P n -> P (n.+1)) + -> (forall n : nat, P (- n) -> P (- (n.+1))) + -> forall n : int, P n. +Proof. +by move=> P0 hPp hPn []; elim=> [|n ihn]//; do? [apply: hPn | apply: hPp]. +Qed. + +Definition int_rec := int_rect. +Definition int_ind := int_rect. + +CoInductive int_spec (x : int) : int -> Type := +| ZintNull of x = 0 : int_spec x 0 +| ZintPos n of x = n.+1 : int_spec x n.+1 +| ZintNeg n of x = - (n.+1)%:Z : int_spec x (- n.+1). + +Lemma intP x : int_spec x x. Proof. by move: x=> [] []; constructor. Qed. + +Lemma addzC : commutative addz. +Proof. by move=> [] m [] n //=; rewrite addnC. Qed. + +Lemma add0z : left_id 0 addz. Proof. by move=> [] [|]. Qed. + +Lemma oppzK : involutive oppz. Proof. by do 2?case. Qed. + +Lemma oppz_add : {morph oppz : m n / m + n}. +Proof. +move=> [[|n]|n] [[|m]|m] /=; rewrite ?NegzE ?oppzK ?addnS ?addn0 ?subn0 //; + rewrite ?ltnS[m <= n]leqNgt [n <= m]leqNgt; case: ltngtP=> hmn /=; + by rewrite ?hmn ?subnn // ?oppzK ?subSS ?subnS ?prednK // ?subn_gt0. +Qed. + +Lemma add1Pz (n : int) : 1 + (n - 1) = n. +Proof. by case: (intP n)=> // n' /= _; rewrite ?(subn1, addn0). Qed. + +Lemma subSz1 (n : int) : 1 + n - 1 = n. +Proof. +by apply: (inv_inj oppzK); rewrite addzC !oppz_add oppzK [_ - n]addzC add1Pz. +Qed. + +Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n). +Proof. +move: m n=> [|m] [] [|n] //=; rewrite ?add1n ?subn1 // !(ltnS, subSS). +rewrite [n <= m]leqNgt; case: ltngtP=> hmn /=; rewrite ?hmn ?subnn //. + by rewrite subnS add1n prednK ?subn_gt0. +by rewrite ltnS leqn0 subn_eq0 leqNgt hmn /= subnS subn1. +Qed. + +Lemma addSz (m n : int) : (1 + m) + n = 1 + (m + n). +Proof. +case: m => [] m; first by rewrite -PoszD add1n addSnz. +rewrite !NegzE; apply: (inv_inj oppzK). +rewrite !oppz_add !oppzK addSnz [-1%:Z + _]addzC addSnz add1Pz. +by rewrite [-1%:Z + _]addzC subSz1. +Qed. + +Lemma addPz (m n : int) : (m - 1) + n = (m + n) - 1. +Proof. +by apply: (inv_inj oppzK); rewrite !oppz_add oppzK [_ + 1]addzC addSz addzC. +Qed. + +Lemma addzA : associative addz. +Proof. +elim=> [|m ihm|m ihm] n p; first by rewrite !add0z. + by rewrite -add1n PoszD !addSz ihm. +by rewrite -add1n addnC PoszD oppz_add !addPz ihm. +Qed. + +Lemma addNz : left_inverse (0:int) oppz addz. Proof. by do 3?elim. Qed. + +Lemma predn_int (n : nat) : 0 < n -> n.-1%:Z = n - 1. +Proof. by case: n=> // n _ /=; rewrite subn1. Qed. + +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}. Proof. by []. Qed. + +Lemma NegzE (n : nat) : Negz n = -(n.+1)%:Z. Proof. by []. Qed. + +Lemma int_rect (P : int -> Type) : + P 0 -> (forall n : nat, P n -> P (n.+1)%N) + -> (forall n : nat, P (- (n%:Z)) -> P (- (n.+1%N%:Z))) + -> forall n : int, P n. +Proof. +by move=> P0 hPp hPn []; elim=> [|n ihn]//; do? [apply: hPn | apply: hPp]. +Qed. + +Definition int_rec := int_rect. +Definition int_ind := int_rect. + +CoInductive int_spec (x : int) : int -> Type := +| ZintNull : int_spec x 0 +| ZintPos n : int_spec x n.+1 +| ZintNeg n : int_spec x (- (n.+1)%:Z). + +Lemma intP x : int_spec x x. +Proof. by move: x=> [] [] *; rewrite ?NegzE; constructor. Qed. + +Definition oppz_add := (@opprD [zmodType of int]). + +Lemma subzn (m n : nat) : (n <= m)%N -> m%:Z - n%:Z = (m - n)%N. +Proof. +elim: n=> //= [|n ihn] hmn; first by rewrite subr0 subn0. +rewrite subnS -addn1 !PoszD opprD addrA ihn 1?ltnW //. +by rewrite intZmod.predn_int // subn_gt0. +Qed. + +Lemma subzSS (m n : nat) : m.+1%:Z - n.+1%:Z = m%:Z - n%:Z. +Proof. by elim: n m=> [|n ihn] m //; rewrite !subzn. Qed. + +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. +Proof. by case=> [n|[|n]] //=; rewrite muln0. Qed. + +Lemma mulzC : commutative mulz. +Proof. by move=> [] m [] n //=; rewrite mulnC. Qed. + +Lemma mulz0 : right_zero 0 *%Z. +Proof. by move=> x; rewrite mulzC mul0z. Qed. + +Lemma mulzN (m n : int) : (m * (- n))%Z = - (m * n)%Z. +Proof. +by case: (intP m)=> {m} [|m|m]; rewrite ?mul0z //; +case: (intP n)=> {n} [|n|n]; rewrite ?mulz0 //= mulnC. +Qed. + +Lemma mulNz (m n : int) : ((- m) * n)%Z = - (m * n)%Z. +Proof. by rewrite mulzC mulzN mulzC. Qed. + +Lemma mulzA : associative mulz. +Proof. +by move=> [] m [] n [] p; rewrite ?NegzE ?(mulnA,mulNz,mulzN,opprK) //= ?mulnA. +Qed. + +Lemma mul1z : left_id 1%Z mulz. +Proof. by case=> [[|n]|n] //=; rewrite ?mul1n// plusE addn0. Qed. + +Lemma mulzS (x : int) (n : nat) : (x * n.+1%:Z)%Z = x + (x * n)%Z. +Proof. +by case: (intP x)=> [|m'|m'] //=; [rewrite mulnS|rewrite mulSn -opprD]. +Qed. + +Lemma mulz_addl : left_distributive mulz (+%R). +Proof. +move=> x y z; elim: z=> [|n|n]; first by rewrite !(mul0z,mulzC). + by rewrite !mulzS=> ->; rewrite !addrA [X in X + _]addrAC. +rewrite !mulzN !mulzS -!opprD=> /(inv_inj (@opprK _))->. +by rewrite !addrA [X in X + _]addrAC. +Qed. + +Lemma nonzero1z : 1%Z != 0. Proof. by []. Qed. + +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}. Proof. by []. Qed. + +Lemma intS (n : nat) : n.+1%:Z = 1 + n%:Z. Proof. by rewrite -PoszD. Qed. + +Lemma predn_int (n : nat) : (0 < n)%N -> n.-1%:Z = n%:Z - 1. +Proof. exact: intZmod.predn_int. Qed. + +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}. +Proof. by move=> n /pred2P[] ->. Qed. + +Lemma mulzn_eq1 m (n : nat) : (m * n == 1) = (m == 1) && (n == 1%N). +Proof. by case: m=> m /=; [rewrite -PoszM [_==_]muln_eq1 | case: n]. Qed. + +Lemma unitzPl m n : n * m = 1 -> m \is a unitz. +Proof. +case: m => m; move/eqP; rewrite qualifE. +* by rewrite mulzn_eq1; case/andP=> _; move/eqP->. +* by rewrite NegzE intS mulrN -mulNr mulzn_eq1; case/andP=> _. +Qed. + +Lemma invz_out : {in [predC unitz], invz =1 id}. +Proof. exact. Qed. + +Lemma idomain_axiomz m n : m * n = 0 -> (m == 0) || (n == 0). +Proof. +by case: m n => m [] n //=; move/eqP; rewrite ?(NegzE,mulrN,mulNr); + rewrite ?(inv_eq (@opprK _)) -PoszM [_==_]muln_eq0. +Qed. + +Definition comMixin := ComUnitRingMixin mulVz unitzPl invz_out. + +End intUnitRing. +End intUnitRing. + +Canonical int_unitRingType := + Eval hnf in UnitRingType int intUnitRing.comMixin. +Canonical int_comUnitRing := Eval hnf in [comUnitRingType of int]. +Canonical int_iDomain := + Eval hnf in IdomainType int intUnitRing.idomain_axiomz. + +Definition absz m := match m with Posz p => p | Negz n => n.+1 end. +Notation "m - n" := + (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. +Arguments Scope absz [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). +Proof. +move: x y=> [] m [] n; rewrite /= ?addnS //=; +rewrite /GRing.add /GRing.Zmodule.add /=; case: ltnP=> //=; +rewrite ?addSn ?ltnS ?leq_subLR ?(addnS, addSn) ?(leq_trans _ (leqnSn _)) //; +by rewrite 1?addnCA ?leq_addr ?addnA ?leq_addl. +Qed. + +Fact ltz_add x y : ltz 0 x -> ltz 0 y -> ltz 0 (x + y). +Proof. by move: x y => [] x [] y //= hx hy; rewrite ltn_addr. Qed. + +Fact eq0_normz x : normz x = 0 -> x = 0. Proof. by case: x. Qed. + +Fact lez_total x y : lez x y || lez y x. +Proof. by move: x y => [] x [] y //=; apply: leq_total. Qed. + +Lemma abszN (n : nat) : absz (- n%:Z) = n. Proof. by case: n. Qed. + +Fact normzM : {morph (fun n => normz n) : x y / x * y}. +Proof. by move=> [] x [] y; rewrite // abszN // mulnC. Qed. + +Lemma subz_ge0 m n : lez 0 (n - m) = lez m n. +Proof. +case: (intP m); case: (intP n)=> // {m n} m n /=; +rewrite ?ltnS -?opprD ?opprB ?subzSS; case: leqP=> // hmn; +by [ rewrite subzn // + | rewrite -opprB subzn ?(ltnW hmn) //; + move: hmn; rewrite -subn_gt0; case: (_ - _)%N]. +Qed. + +Fact lez_def x y : (lez x y) = (normz (y - x) == y - x). +Proof. by rewrite -subz_ge0; move: (_ - _) => [] n //=; rewrite eqxx. Qed. + +Fact ltz_def x y : (ltz x y) = (y != x) && (lez x y). +Proof. +by move: x y=> [] x [] y //=; rewrite (ltn_neqAle, leq_eqVlt) // eq_sym. +Qed. + +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. +Proof. by []. Qed. + +Lemma ltz_nat m n : (m < n :> int) = (m < n)%N. +Proof. by rewrite ltnNge ltrNge lez_nat. Qed. + +Definition ltez_nat := (lez_nat, ltz_nat). + +Lemma leNz_nat m n : (- m%:Z <= n). Proof. by case: m. Qed. + +Lemma ltNz_nat m n : (- m%:Z < n) = (m != 0%N) || (n != 0%N). +Proof. by move: m n=> [|?] []. Qed. + +Definition lteNz_nat := (leNz_nat, ltNz_nat). + +Lemma lezN_nat m n : (m%:Z <= - n%:Z) = (m == 0%N) && (n == 0%N). +Proof. by move: m n=> [|?] []. Qed. + +Lemma ltzN_nat m n : (m%:Z < - n%:Z) = false. +Proof. by move: m n=> [|?] []. Qed. + +Lemma le0z_nat n : 0 <= n :> int. Proof. by []. Qed. + +Lemma lez0_nat n : n <= 0 :> int = (n == 0%N :> nat). Proof. by elim: n. Qed. + +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). Proof. by case: (intP x). Qed. + +Lemma lez_add1r x y : (1 + x <= y) = (x < y). +Proof. by rewrite -subr_gt0 gtz0_ge1 lter_sub_addr. Qed. + +Lemma lez_addr1 x y : (x + 1 <= y) = (x < y). +Proof. by rewrite addrC lez_add1r. Qed. + +Lemma ltz_add1r x y : (x < 1 + y) = (x <= y). +Proof. by rewrite -lez_add1r ler_add2l. Qed. + +Lemma ltz_addr1 x y : (x < y + 1) = (x <= y). +Proof. by rewrite -lez_addr1 ler_add2r. Qed. + +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") : 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. +Proof. by []. Qed. + +Lemma nmulrn (R : zmodType) (x : R) (n : nat) : x *- n = x *~ - n%:Z. +Proof. by case: n=> [] //; rewrite ?oppr0. Qed. + +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). +Proof. +elim: m=> [|m _|m _]; elim: n=> [|n _|n _]; rewrite /intmul //=; +rewrite ?(muln0, mulr0n, mul0rn, oppr0, mulNrn, opprK) //; + do ?by rewrite mulnC mulrnA. +* by rewrite -mulrnA mulnC. +* by rewrite -mulrnA. +Qed. + +Fact mulrzAC m n x : (x *~ n) *~ m = (x *~ m) *~ n. +Proof. by rewrite !mulrzA_C mulrC. Qed. + +Fact mulr1z (x : M) : x *~ 1 = x. Proof. by []. Qed. + +Fact mulrzDr m : {morph ( *~%R^~ m : M -> M) : x y / x + y}. +Proof. +by elim: m=> [|m _|m _] x y; + rewrite ?addr0 /intmul //= ?mulrnDl // opprD. +Qed. + +Lemma mulrzBl_nat (m n : nat) x : x *~ (m%:Z - n%:Z) = x *~ m - x *~ n. +Proof. +case: (leqP m n)=> hmn; rewrite /intmul //=. + rewrite addrC -{1}[m:int]opprK -opprD subzn //. + rewrite -{2}[n](@subnKC m)// mulrnDr opprD addrA subrr sub0r. + by case hdmn: (_ - _)%N=> [|dmn] /=; first by rewrite mulr0n oppr0. +have hnm := ltnW hmn. +rewrite -{2}[m](@subnKC n)// mulrnDr addrAC subrr add0r. +by rewrite subzn. +Qed. + +Fact mulrzDl x : {morph *~%R x : m n / m + n}. +Proof. +elim=> [|m _|m _]; elim=> [|n _|n _]; rewrite /intmul //=; +rewrite -?(opprD) ?(add0r, addr0, mulrnDr, subn0) //. +* by rewrite -/(intmul _ _) mulrzBl_nat. +* by rewrite -/(intmul _ _) addrC mulrzBl_nat addrC. +* by rewrite -addnS -addSn mulrnDr. +Qed. + +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. Proof. by []. Qed. + +Lemma mulrzA x m n : x *~ (m * n) = x *~ m *~ n. +Proof. by rewrite -!scalezrE scalerA mulrC. Qed. + +Lemma mulr0z x : x *~ 0 = 0. Proof. by []. Qed. + +Lemma mul0rz n : 0 *~ n = 0 :> M. +Proof. by rewrite -scalezrE scaler0. Qed. + +Lemma mulrNz x n : x *~ (- n) = - (x *~ n). +Proof. by rewrite -scalezrE scaleNr. Qed. + +Lemma mulrN1z x : x *~ (- 1) = - x. Proof. by rewrite -scalezrE scaleN1r. Qed. + +Lemma mulNrz x n : (- x) *~ n = - (x *~ n). +Proof. by rewrite -scalezrE scalerN. Qed. + +Lemma mulrzBr x m n : x *~ (m - n) = x *~ m - x *~ n. +Proof. by rewrite -scalezrE scalerBl. Qed. + +Lemma mulrzBl x y n : (x - y) *~ n = x *~ n - y *~ n. +Proof. by rewrite -scalezrE scalerBr. Qed. + +Lemma mulrz_nat (n : nat) x : x *~ n%:R = x *+ n. +Proof. by rewrite -scalezrE scaler_nat. Qed. + +Lemma mulrz_sumr : forall x I r (P : pred I) F, + x *~ (\sum_(i <- r | P i) F i) = \sum_(i <- r | P i) x *~ F i. +Proof. by rewrite -/M^z; exact: scaler_suml. Qed. + +Lemma mulrz_suml : forall 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. +Proof. by rewrite -/M^z; exact: scaler_sumr. Qed. + +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. +Proof. by case: z => n; rewrite ?ffunE ffunMnE. Qed. + +Lemma intz (n : int) : n%:~R = n. +Proof. +elim: n=> //= n ihn; rewrite /intmul /=. + by rewrite -addn1 mulrnDr /= PoszD -ihn. +by rewrite nmulrn intS opprD mulrzDl ihn. +Qed. + +Lemma natz (n : nat) : n%:R = n%:Z :> int. +Proof. by rewrite pmulrn intz. Qed. + +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. +Proof. +by elim: n=> //= *; rewrite ?mul0r ?mulr0z // /intmul /= -mulrnAl -?mulNr. +Qed. + +Lemma mulrzAr n x y : x * (y *~ n) = (x * y) *~ n. +Proof. +by elim: n=> //= *; rewrite ?mulr0 ?mulr0z // /intmul /= -mulrnAr -?mulrN. +Qed. + +Lemma mulrzl x n : n%:~R * x = x *~ n. +Proof. by rewrite mulrzAl mul1r. Qed. + +Lemma mulrzr x n : x * n%:~R = x *~ n. +Proof. by rewrite mulrzAr mulr1. Qed. + +Lemma mulNrNz n x : (-x) *~ (-n) = x *~ n. +Proof. by rewrite mulNrz mulrNz opprK. Qed. + +Lemma mulrbz x (b : bool) : x *~ b = (if b then x else 0). +Proof. by case: b. Qed. + +Lemma intrD m n : (m + n)%:~R = m%:~R + n%:~R :> R. +Proof. exact: mulrzDl. Qed. + +Lemma intrM m n : (m * n)%:~R = m%:~R * n%:~R :> R. +Proof. by rewrite mulrzA -mulrzr. Qed. + +Lemma intmul1_is_rmorphism : rmorphism ( *~%R (1 : R)). +Proof. +by do ?split; move=> // x y /=; rewrite ?intrD ?mulrNz ?intrM. +Qed. +Canonical intmul1_rmorphism := RMorphism intmul1_is_rmorphism. + +Lemma mulr2z n : n *~ 2 = n + n. Proof. exact: mulr2n. Qed. + +End RintMod. + +Lemma mulrzz m n : m *~ n = m * n. Proof. by rewrite -mulrzr intz. Qed. + +Lemma mulz2 n : n * 2%:Z = n + n. Proof. by rewrite -mulrzz. Qed. + +Lemma mul2z n : 2%:Z * n = n + n. Proof. by rewrite mulrC -mulrzz. Qed. + +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. +Proof. +elim: n=> [|n ihn|n ihn]; first by rewrite scale0r. + by rewrite intS !mulrzDl scalerDl ihn scale1r. +by rewrite intS opprD !mulrzDl scalerDl ihn scaleN1r. +Qed. + +Lemma scalerMzl a v n : (a *: v) *~ n = (a *~ n) *: v. +Proof. by rewrite -mulrzl -scaler_int scalerA. Qed. + +Lemma scalerMzr a v n : (a *: v) *~ n = a *: (v *~ n). +Proof. by rewrite -!scaler_int !scalerA mulrzr mulrzl. Qed. + +End LMod. + +Lemma mulrz_int (M : zmodType) (n : int) (x : M) : x *~ n%:~R = x *~ n. +Proof. by rewrite -scalezrE scaler_int. Qed. + +Section MorphTheory. +Local Coercion Posz : nat >-> int. +Section Additive. +Variables (U V : zmodType) (f : {additive U -> V}). + +Lemma raddfMz n : {morph f : x / x *~ n}. +Proof. +case: n=> n x /=; first exact: raddfMn. +by rewrite NegzE !mulrNz; apply: raddfMNn. +Qed. + +End Additive. + +Section Multiplicative. + +Variables (R S : ringType) (f : {rmorphism R -> S}). + +Lemma rmorphMz : forall n, {morph f : x / x *~ n}. Proof. exact: raddfMz. Qed. + +Lemma rmorph_int : forall n, f n%:~R = n%:~R. +Proof. by move=> n; rewrite rmorphMz rmorph1. Qed. + +End Multiplicative. + +Section Linear. + +Variable R : ringType. +Variables (U V : lmodType R) (f : {linear U -> V}). + +Lemma linearMn : forall n, {morph f : x / x *~ n}. Proof. exact: raddfMz. Qed. + +End Linear. + +Lemma raddf_int_scalable (aV rV : lmodType int) (f : {additive aV -> rV}) : + scalable f. +Proof. by move=> z u; rewrite -[z]intz !scaler_int raddfMz. Qed. + +Section Zintmul1rMorph. + +Variable R : ringType. + +Lemma commrMz (x y : R) n : GRing.comm x y -> GRing.comm x (y *~ n). +Proof. by rewrite /GRing.comm=> com_xy; rewrite mulrzAr mulrzAl com_xy. Qed. + +Lemma commr_int (x : R) n : GRing.comm x n%:~R. +Proof. by apply: commrMz; apply: commr1. Qed. + +End Zintmul1rMorph. + +Section ZintBigMorphism. + +Variable R : ringType. + +Lemma sumMz : forall I r (P : pred I) F, + (\sum_(i <- r | P i) F i)%N%:~R = \sum_(i <- r | P i) ((F i)%:~R) :> R. +Proof. by apply: big_morph=> // x y; rewrite !pmulrn -rmorphD. Qed. + +Lemma prodMz : forall I r (P : pred I) F, + (\prod_(i <- r | P i) F i)%N%:~R = \prod_(i <- r | P i) ((F i)%:~R) :> R. +Proof. by apply: big_morph=> // x y; rewrite !pmulrn PoszM -rmorphM. Qed. + +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. +Proof. +case: n=> n /=; first exact: Frobenius_autMn. +by rewrite !NegzE !mulrNz Frobenius_autN Frobenius_autMn. +Qed. + +Lemma Frobenius_aut_int n : (n%:~R)^f = n%:~R. +Proof. by rewrite Frobenius_autMz Frobenius_aut1. Qed. + +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). +Proof. +move=> n; wlog : n / 0 <= n; case: n=> [] n //; do ?exact. + by rewrite NegzE !rmorphN=>->. +move=> _; elim: n=> [|n ihn]; first by rewrite rmorph0. +by rewrite intS !rmorphD !rmorph1 ihn. +Qed. + +(* intmul and ler/ltr *) +Lemma ler_pmulz2r n (hn : 0 < n) : {mono *~%R^~ n :x y / x <= y :> R}. +Proof. by move=> x y; case: n hn=> [[]|] // n _; rewrite ler_pmuln2r. Qed. + +Lemma ltr_pmulz2r n (hn : 0 < n) : {mono *~%R^~ n : x y / x < y :> R}. +Proof. exact: lerW_mono (ler_pmulz2r _). Qed. + +Lemma ler_nmulz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x <= y :> R}. +Proof. +move=> x y /=; rewrite -![_ *~ n]mulNrNz. +by rewrite ler_pmulz2r (oppr_cp0, ler_opp2). +Qed. + +Lemma ltr_nmulz2r n (hn : n < 0) : {mono *~%R^~ n : x y /~ x < y :> R}. +Proof. exact: lerW_nmono (ler_nmulz2r _). Qed. + +Lemma ler_wpmulz2r n (hn : 0 <= n) : {homo *~%R^~ n : x y / x <= y :> R}. +Proof. by move=> x y xy; case: n hn=> [] // n _; rewrite ler_wmuln2r. Qed. + +Lemma ler_wnmulz2r n (hn : n <= 0) : {homo *~%R^~ n : x y /~ x <= y :> R}. +Proof. +by move=> x y xy /=; rewrite -ler_opp2 -!mulrNz ler_wpmulz2r // oppr_ge0. +Qed. + +Lemma mulrz_ge0 x n (x0 : 0 <= x) (n0 : 0 <= n) : 0 <= x *~ n. +Proof. by rewrite -(mul0rz _ n) ler_wpmulz2r. Qed. + +Lemma mulrz_le0 x n (x0 : x <= 0) (n0 : n <= 0) : 0 <= x *~ n. +Proof. by rewrite -(mul0rz _ n) ler_wnmulz2r. Qed. + +Lemma mulrz_ge0_le0 x n (x0 : 0 <= x) (n0 : n <= 0) : x *~ n <= 0. +Proof. by rewrite -(mul0rz _ n) ler_wnmulz2r. Qed. + +Lemma mulrz_le0_ge0 x n (x0 : x <= 0) (n0 : 0 <= n) : x *~ n <= 0. +Proof. by rewrite -(mul0rz _ n) ler_wpmulz2r. Qed. + +Lemma pmulrz_lgt0 x n (n0 : 0 < n) : 0 < x *~ n = (0 < x). +Proof. by rewrite -(mul0rz _ n) ltr_pmulz2r // mul0rz. Qed. + +Lemma nmulrz_lgt0 x n (n0 : n < 0) : 0 < x *~ n = (x < 0). +Proof. by rewrite -(mul0rz _ n) ltr_nmulz2r // mul0rz. Qed. + +Lemma pmulrz_llt0 x n (n0 : 0 < n) : x *~ n < 0 = (x < 0). +Proof. by rewrite -(mul0rz _ n) ltr_pmulz2r // mul0rz. Qed. + +Lemma nmulrz_llt0 x n (n0 : n < 0) : x *~ n < 0 = (0 < x). +Proof. by rewrite -(mul0rz _ n) ltr_nmulz2r // mul0rz. Qed. + +Lemma pmulrz_lge0 x n (n0 : 0 < n) : 0 <= x *~ n = (0 <= x). +Proof. by rewrite -(mul0rz _ n) ler_pmulz2r // mul0rz. Qed. + +Lemma nmulrz_lge0 x n (n0 : n < 0) : 0 <= x *~ n = (x <= 0). +Proof. by rewrite -(mul0rz _ n) ler_nmulz2r // mul0rz. Qed. + +Lemma pmulrz_lle0 x n (n0 : 0 < n) : x *~ n <= 0 = (x <= 0). +Proof. by rewrite -(mul0rz _ n) ler_pmulz2r // mul0rz. Qed. + +Lemma nmulrz_lle0 x n (n0 : n < 0) : x *~ n <= 0 = (0 <= x). +Proof. by rewrite -(mul0rz _ n) ler_nmulz2r // mul0rz. Qed. + +Lemma ler_wpmulz2l x (hx : 0 <= x) : {homo *~%R x : x y / x <= y}. +Proof. +by move=> m n /= hmn; rewrite -subr_ge0 -mulrzBr mulrz_ge0 // subr_ge0. +Qed. + +Lemma ler_wnmulz2l x (hx : x <= 0) : {homo *~%R x : x y /~ x <= y}. +Proof. +by move=> m n /= hmn; rewrite -subr_ge0 -mulrzBr mulrz_le0 // subr_le0. +Qed. + +Lemma ler_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x <= y}. +Proof. +move=> m n /=; rewrite real_mono ?num_real // => {m n}. +by move=> m n /= hmn; rewrite -subr_gt0 -mulrzBr pmulrz_lgt0 // subr_gt0. +Qed. + +Lemma ler_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x <= y}. +Proof. +move=> m n /=; rewrite real_nmono ?num_real // => {m n}. +by move=> m n /= hmn; rewrite -subr_gt0 -mulrzBr nmulrz_lgt0 // subr_lt0. +Qed. + +Lemma ltr_pmulz2l x (hx : 0 < x) : {mono *~%R x : x y / x < y}. +Proof. exact: lerW_mono (ler_pmulz2l _). Qed. + +Lemma ltr_nmulz2l x (hx : x < 0) : {mono *~%R x : x y /~ x < y}. +Proof. exact: lerW_nmono (ler_nmulz2l _). Qed. + +Lemma pmulrz_rgt0 x n (x0 : 0 < x) : 0 < x *~ n = (0 < n). +Proof. by rewrite -(mulr0z x) ltr_pmulz2l. Qed. + +Lemma nmulrz_rgt0 x n (x0 : x < 0) : 0 < x *~ n = (n < 0). +Proof. by rewrite -(mulr0z x) ltr_nmulz2l. Qed. + +Lemma pmulrz_rlt0 x n (x0 : 0 < x) : x *~ n < 0 = (n < 0). +Proof. by rewrite -(mulr0z x) ltr_pmulz2l. Qed. + +Lemma nmulrz_rlt0 x n (x0 : x < 0) : x *~ n < 0 = (0 < n). +Proof. by rewrite -(mulr0z x) ltr_nmulz2l. Qed. + +Lemma pmulrz_rge0 x n (x0 : 0 < x) : 0 <= x *~ n = (0 <= n). +Proof. by rewrite -(mulr0z x) ler_pmulz2l. Qed. + +Lemma nmulrz_rge0 x n (x0 : x < 0) : 0 <= x *~ n = (n <= 0). +Proof. by rewrite -(mulr0z x) ler_nmulz2l. Qed. + +Lemma pmulrz_rle0 x n (x0 : 0 < x) : x *~ n <= 0 = (n <= 0). +Proof. by rewrite -(mulr0z x) ler_pmulz2l. Qed. + +Lemma nmulrz_rle0 x n (x0 : x < 0) : x *~ n <= 0 = (0 <= n). +Proof. by rewrite -(mulr0z x) ler_nmulz2l. Qed. + +Lemma mulrIz x (hx : x != 0) : injective ( *~%R x). +Proof. +move=> y z; rewrite -![x *~ _]mulrzr => /(mulfI hx). +by apply: mono_inj y z; apply: ler_pmulz2l. +Qed. + +Lemma ler_int m n : (m%:~R <= n%:~R :> R) = (m <= n). +Proof. by rewrite ler_pmulz2l. Qed. + +Lemma ltr_int m n : (m%:~R < n%:~R :> R) = (m < n). +Proof. by rewrite ltr_pmulz2l. Qed. + +Lemma eqr_int m n : (m%:~R == n%:~R :> R) = (m == n). +Proof. by rewrite (inj_eq (mulrIz _)) ?oner_eq0. Qed. + +Lemma ler0z n : (0 <= n%:~R :> R) = (0 <= n). +Proof. by rewrite pmulrz_rge0. Qed. + +Lemma ltr0z n : (0 < n%:~R :> R) = (0 < n). +Proof. by rewrite pmulrz_rgt0. Qed. + +Lemma lerz0 n : (n%:~R <= 0 :> R) = (n <= 0). +Proof. by rewrite pmulrz_rle0. Qed. + +Lemma ltrz0 n : (n%:~R < 0 :> R) = (n < 0). +Proof. by rewrite pmulrz_rlt0. Qed. + +Lemma ler1z (n : int) : (1 <= n%:~R :> R) = (1 <= n). +Proof. by rewrite -[1]/(1%:~R) ler_int. Qed. + +Lemma ltr1z (n : int) : (1 < n%:~R :> R) = (1 < n). +Proof. by rewrite -[1]/(1%:~R) ltr_int. Qed. + +Lemma lerz1 n : (n%:~R <= 1 :> R) = (n <= 1). +Proof. by rewrite -[1]/(1%:~R) ler_int. Qed. + +Lemma ltrz1 n : (n%:~R < 1 :> R) = (n < 1). +Proof. by rewrite -[1]/(1%:~R) ltr_int. Qed. + +Lemma intr_eq0 n : (n%:~R == 0 :> R) = (n == 0). +Proof. by rewrite -(mulr0z 1) (inj_eq (mulrIz _)) // oner_eq0. Qed. + +Lemma mulrz_eq0 x n : (x *~ n == 0) = ((n == 0) || (x == 0)). +Proof. by rewrite -mulrzl mulf_eq0 intr_eq0. Qed. + +Lemma mulrz_neq0 x n : x *~ n != 0 = ((n != 0) && (x != 0)). +Proof. by rewrite mulrz_eq0 negb_or. Qed. + +Lemma realz n : (n%:~R : R) \in Num.real. +Proof. by rewrite -topredE /Num.real /= ler0z lerz0 ler_total. Qed. +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 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. +Local Coercion Posz : nat >-> int. + +Lemma exprnP x (n : nat) : x ^+ n = x ^ n. Proof. by []. Qed. + +Lemma exprnN x (n : nat) : x ^- n = x ^ -n%:Z. +Proof. by case: n=> //; rewrite oppr0 expr0 invr1. Qed. + +Lemma expr0z x : x ^ 0 = 1. Proof. by []. Qed. + +Lemma expr1z x : x ^ 1 = x. Proof. by []. Qed. + +Lemma exprN1 x : x ^ (-1) = x^-1. Proof. by []. Qed. + +Lemma invr_expz x n : (x ^ n)^-1 = x ^ (- n). +Proof. +by case: (intP n)=> // [|m]; rewrite ?opprK ?expr0z ?invr1 // invrK. +Qed. + +Lemma exprz_inv x n : (x^-1) ^ n = x ^ (- n). +Proof. +by case: (intP n)=> // m; rewrite -[_ ^ (- _)]exprVn ?opprK ?invrK. +Qed. + +Lemma exp1rz n : 1 ^ n = 1 :> R. +Proof. +by case: (intP n)=> // m; rewrite -?exprz_inv ?invr1; apply: expr1n. +Qed. + +Lemma exprSz x (n : nat) : x ^ n.+1 = x * x ^ n. Proof. exact: exprS. Qed. + +Lemma exprSzr x (n : nat) : x ^ n.+1 = x ^ n * x. +Proof. exact: exprSr. Qed. + +Fact exprzD_nat x (m n : nat) : x ^ (m%:Z + n) = x ^ m * x ^ n. +Proof. exact: exprD. Qed. + +Fact exprzD_Nnat x (m n : nat) : x ^ (-m%:Z + -n%:Z) = x ^ (-m%:Z) * x ^ (-n%:Z). +Proof. by rewrite -opprD -!exprz_inv exprzD_nat. Qed. + +Lemma exprzD_ss x m n : (0 <= m) && (0 <= n) || (m <= 0) && (n <= 0) + -> x ^ (m + n) = x ^ m * x ^ n. +Proof. +case: (intP m)=> {m} [|m|m]; case: (intP n)=> {n} [|n|n] //= _; +by rewrite ?expr0z ?mul1r ?exprzD_nat ?exprzD_Nnat ?sub0r ?addr0 ?mulr1. +Qed. + +Lemma exp0rz n : 0 ^ n = (n == 0)%:~R :> R. +Proof. by case: (intP n)=> // m; rewrite -?exprz_inv ?invr0 exprSz mul0r. Qed. + +Lemma commrXz x y n : GRing.comm x y -> GRing.comm x (y ^ n). +Proof. +rewrite /GRing.comm; elim: n x y=> [|n ihn|n ihn] x y com_xy //=. +* by rewrite expr0z mul1r mulr1. +* by rewrite -exprnP commrX //. +rewrite -exprz_inv -exprnP commrX //. +case: (boolP (y \is a GRing.unit))=> uy; last by rewrite invr_out. +by apply/eqP; rewrite (can2_eq (mulrVK _) (mulrK _)) // -mulrA com_xy mulKr. +Qed. + +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. +Proof. +move=> ux uy com_xy; elim: n => [|n _|n _]; first by rewrite expr0z mulr1. + by rewrite -!exprnP exprMn_comm. +rewrite -!exprnN -!exprVn com_xy -exprMn_comm ?invrM//. +exact/commrV/commr_sym/commrV. +Qed. + +Lemma commrXz_wmulls x y n : + 0 <= n -> GRing.comm x y -> (x * y) ^ n = x ^ n * y ^ n. +Proof. +move=> n0 com_xy; elim: n n0 => [|n _|n _] //; first by rewrite expr0z mulr1. +by rewrite -!exprnP exprMn_comm. +Qed. + +Lemma unitrXz x n (ux : x \is a GRing.unit) : x ^ n \is a GRing.unit. +Proof. +case: (intP n)=> {n} [|n|n]; rewrite ?expr0z ?unitr1 ?unitrX //. +by rewrite -invr_expz unitrV unitrX. +Qed. + +Lemma exprzDr x (ux : x \is a GRing.unit) m n : x ^ (m + n) = x ^ m * x ^ n. +Proof. +move: n m; apply: wlog_ler=> n m hnm. + by rewrite addrC hnm commrXz //; apply: commr_sym; apply: commrXz. +case: (intP m) hnm=> {m} [|m|m]; rewrite ?mul1r ?add0r //; + case: (intP n)=> {n} [|n|n _]; rewrite ?mulr1 ?addr0 //; + do ?by rewrite exprzD_ss. +rewrite -invr_expz subzSS !exprSzr invrM ?unitrX // -mulrA mulVKr //. +case: (leqP n m)=> [|/ltnW] hmn; rewrite -{2}(subnK hmn) exprzD_nat -subzn //. + by rewrite mulrK ?unitrX. +by rewrite invrM ?unitrXz // mulVKr ?unitrXz // -opprB -invr_expz. +Qed. + +Lemma exprz_exp x m n : (x ^ m) ^ n = (x ^ (m * n)). +Proof. +wlog: n / 0 <= n. + by case: n=> [n -> //|n]; rewrite ?NegzE mulrN -?invr_expz=> -> /=. +elim: n x m=> [|n ihn|n ihn] x m // _; first by rewrite mulr0 !expr0z. +rewrite exprSz ihn // intS mulrDr mulr1 exprzD_ss //. +by case: (intP m)=> // m'; rewrite ?oppr_le0 //. +Qed. + +Lemma exprzAC x m n : (x ^ m) ^ n = (x ^ n) ^ m. +Proof. by rewrite !exprz_exp mulrC. Qed. + +Lemma exprz_out x n (nux : x \isn't a GRing.unit) (hn : 0 <= n) : + x ^ (- n) = x ^ n. +Proof. by case: (intP n) hn=> //= m; rewrite -exprnN -exprVn invr_out. Qed. + +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). +Proof. +by elim: n=> [|n ihn|n _] // _; rewrite !exprSz ihn // mulrzAr mulrzAl -mulrzA. +Qed. + +Lemma exprz_pintl m n (hn : 0 <= n) : m%:~R ^ n = (m ^ n)%:~R :> R. +Proof. by rewrite exprz_pmulzl // exp1rz. Qed. + +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. +Proof. +rewrite -[x *~ _]mulrzl exprMz_comm //. +by apply: commr_sym; apply: commr_int. +Qed. + +Lemma expNrz x n : (- x) ^ n = (-1) ^ n * x ^ n :> R. +Proof. +case: n=> [] n; rewrite ?NegzE; first by apply: exprNn. +by rewrite -!exprz_inv !invrN invr1; apply: exprNn. +Qed. + +Lemma unitr_n0expz x n : + n != 0 -> (x ^ n \is a GRing.unit) = (x \is a GRing.unit). +Proof. +by case: n => *; rewrite ?NegzE -?exprz_inv ?unitrX_pos ?unitrV ?lt0n. +Qed. + +Lemma intrV (n : int) : + n \in [:: 0; 1; -1] -> n%:~R ^-1 = n%:~R :> R. +Proof. +by case: (intP n)=> // [|[]|[]] //; rewrite ?rmorphN ?invrN (invr0, invr1). +Qed. + +Lemma rmorphXz (R' : unitRingType) (f : {rmorphism R -> R'}) n : + {in GRing.unit, {morph f : x / x ^ n}}. +Proof. by case: n => n x Ux; rewrite ?rmorphV ?rpredX ?rmorphX. Qed. + +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). +Proof. +by case: n=> n; rewrite ?NegzE -?exprz_inv ?expf_eq0 ?lt0n ?invr_eq0. +Qed. + +Lemma expfz_neq0 x n : x != 0 -> x ^ n != 0. +Proof. by move=> x_nz; rewrite expfz_eq0; apply/nandP; right. Qed. + +Lemma exprzMl x y n (ux : x \is a GRing.unit) (uy : y \is a GRing.unit) : + (x * y) ^ n = x ^ n * y ^ n. +Proof. by rewrite exprMz_comm //; apply: mulrC. Qed. + +Lemma expfV (x : R) (i : int) : (x ^ i) ^-1 = (x ^-1) ^ i. +Proof. by rewrite invr_expz exprz_inv. Qed. + +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. +Proof. by move=> hx; rewrite exprzDr ?unitfE. Qed. + +Lemma expfz_n0addr x m n : m + n != 0 -> x ^ (m + n) = x ^ m * x ^ n. +Proof. +have [-> hmn|nx0 _] := eqVneq x 0; last exact: expfzDr. +rewrite !exp0rz (negPf hmn). +case: (altP (m =P 0)) hmn=> [->|]; rewrite (mul0r, mul1r) //. +by rewrite add0r=> /negPf->. +Qed. + +Lemma expfzMl x y n : (x * y) ^ n = x ^ n * y ^ n. +Proof. +have [->|/negPf n0] := eqVneq n 0; first by rewrite !expr0z mulr1. +case: (boolP ((x * y) == 0)); rewrite ?mulf_eq0. + by case/orP=> /eqP->; rewrite ?(mul0r, mulr0, exp0rz, n0). +by case/norP=> x0 y0; rewrite exprzMl ?unitfE. +Qed. + +Lemma fmorphXz (R : unitRingType) (f : {rmorphism F -> R}) n : + {morph f : x / x ^ n}. +Proof. by case: n => n x; rewrite ?fmorphV rmorphX. Qed. + +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). +Proof. by case: n=> n; rewrite ?NegzE -?invr_expz ?invr_ge0 ?exprn_ge0. Qed. + +Lemma exprz_gt0 n x (hx : 0 < x) : (0 < x ^ n). +Proof. by case: n=> n; rewrite ?NegzE -?invr_expz ?invr_gt0 ?exprn_gt0. Qed. + +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}}. +Proof. +move=> [] m [] n; rewrite -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _. +by rewrite lez_nat -?exprnP=> /ler_wiexpn2l; apply. +Qed. + +Lemma ler_wniexpz2l x (x0 : 0 <= x) (x1 : x <= 1) : + {in < 0 &, {homo (exprz x) : x y /~ x <= y}}. +Proof. +move=> [] m [] n; rewrite ?NegzE -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _. +rewrite ler_opp2 lez_nat -?invr_expz=> hmn; move: (x0). +rewrite le0r=> /orP [/eqP->|lx0]; first by rewrite !exp0rz invr0. +by rewrite lef_pinv -?topredE /= ?exprz_gt0 // ler_wiexpn2l. +Qed. + +Fact ler_wpeexpz2l x (x1 : 1 <= x) : + {in >= 0 &, {homo (exprz x) : x y / x <= y}}. +Proof. +move=> [] m [] n; rewrite -!topredE /= ?oppr_cp0 ?ltz_nat // => _ _. +by rewrite lez_nat -?exprnP=> /ler_weexpn2l; apply. +Qed. + +Fact ler_wneexpz2l x (x1 : 1 <= x) : + {in <= 0 &, {homo (exprz x) : x y / x <= y}}. +Proof. +move=> m n hm hn /= hmn. +rewrite -lef_pinv -?topredE /= ?exprz_gt0 ?(ltr_le_trans ltr01) //. +by rewrite !invr_expz ler_wpeexpz2l ?ler_opp2 -?topredE //= oppr_cp0. +Qed. + +Lemma ler_weexpz2l x (x1 : 1 <= x) : {homo (exprz x) : x y / x <= y}. +Proof. +move=> m n /= hmn; case: (lerP 0 m)=> [|/ltrW] hm. + by rewrite ler_wpeexpz2l // [_ \in _](ler_trans hm). +case: (lerP n 0)=> [|/ltrW] hn. + by rewrite ler_wneexpz2l // [_ \in _](ler_trans hmn). +apply: (@ler_trans _ (x ^ 0)); first by rewrite ler_wneexpz2l. +by rewrite ler_wpeexpz2l. +Qed. + +Lemma pexprz_eq1 x n (x0 : 0 <= x) : (x ^ n == 1) = ((n == 0) || (x == 1)). +Proof. +case: n=> n; rewrite ?NegzE -?exprz_inv ?oppr_eq0 pexprn_eq1 // ?invr_eq1 //. +by rewrite invr_ge0. +Qed. + +Lemma ieexprIz x (x0 : 0 < x) (nx1 : x != 1) : injective (exprz x). +Proof. +apply: wlog_ltr=> // m n hmn; first by move=> hmn'; rewrite hmn. +move=> /(f_equal ( *%R^~ (x ^ (- n)))). +rewrite -!expfzDr ?gtr_eqF // subrr expr0z=> /eqP. +by rewrite pexprz_eq1 ?(ltrW x0) // (negPf nx1) subr_eq0 orbF=> /eqP. +Qed. + +Lemma ler_piexpz2l x (x0 : 0 < x) (x1 : x < 1) : + {in >= 0 &, {mono (exprz x) : x y /~ x <= y}}. +Proof. +apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)). + by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF. +by apply: ler_wpiexpz2l; rewrite ?ltrW. +Qed. + +Lemma ltr_piexpz2l x (x0 : 0 < x) (x1 : x < 1) : + {in >= 0 &, {mono (exprz x) : x y /~ x < y}}. +Proof. exact: (lerW_nmono_in (ler_piexpz2l _ _)). Qed. + +Lemma ler_niexpz2l x (x0 : 0 < x) (x1 : x < 1) : + {in < 0 &, {mono (exprz x) : x y /~ x <= y}}. +Proof. +apply: (nhomo_mono_in (nhomo_inj_in_lt _ _)). + by move=> n m hn hm /=; apply: ieexprIz; rewrite // ltr_eqF. +by apply: ler_wniexpz2l; rewrite ?ltrW. +Qed. + +Lemma ltr_niexpz2l x (x0 : 0 < x) (x1 : x < 1) : + {in < 0 &, {mono (exprz x) : x y /~ x < y}}. +Proof. exact: (lerW_nmono_in (ler_niexpz2l _ _)). Qed. + +Lemma ler_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x <= y}. +Proof. +apply: (homo_mono (homo_inj_lt _ _)). + by apply: ieexprIz; rewrite ?(ltr_trans ltr01) // gtr_eqF. +by apply: ler_weexpz2l; rewrite ?ltrW. +Qed. + +Lemma ltr_eexpz2l x (x1 : 1 < x) : {mono (exprz x) : x y / x < y}. +Proof. exact: (lerW_mono (ler_eexpz2l _)). Qed. + +Lemma ler_wpexpz2r n (hn : 0 <= n) : +{in >= 0 & , {homo ((@exprz R)^~ n) : x y / x <= y}}. +Proof. by case: n hn=> // n _; apply: ler_expn2r. Qed. + +Lemma ler_wnexpz2r n (hn : n <= 0) : +{in > 0 & , {homo ((@exprz R)^~ n) : x y /~ x <= y}}. +Proof. +move=> x y /= hx hy hxy; rewrite -lef_pinv ?[_ \in _]exprz_gt0 //. +by rewrite !invr_expz ler_wpexpz2r ?[_ \in _]ltrW // oppr_cp0. +Qed. + +Lemma pexpIrz n (n0 : n != 0) : {in >= 0 &, injective ((@exprz R)^~ n)}. +Proof. +move=> x y; rewrite ![_ \in _]le0r=> /orP [/eqP-> _ /eqP|hx]. + by rewrite exp0rz ?(negPf n0) eq_sym expfz_eq0=> /andP [_ /eqP->]. +case/orP=> [/eqP-> /eqP|hy]. + by rewrite exp0rz ?(negPf n0) expfz_eq0=> /andP [_ /eqP]. +move=> /(f_equal ( *%R^~ (y ^ (- n)))) /eqP. +rewrite -expfzDr ?(gtr_eqF hy) // subrr expr0z -exprz_inv -expfzMl. +rewrite pexprz_eq1 ?(negPf n0) /= ?mulr_ge0 ?invr_ge0 ?ltrW //. +by rewrite (can2_eq (mulrVK _) (mulrK _)) ?unitfE ?(gtr_eqF hy) // mul1r=> /eqP. +Qed. + +Lemma nexpIrz n (n0 : n != 0) : {in <= 0 &, injective ((@exprz R)^~ n)}. +Proof. +move=> x y; rewrite ![_ \in _]ler_eqVlt => /orP [/eqP -> _ /eqP|hx]. + by rewrite exp0rz ?(negPf n0) eq_sym expfz_eq0=> /andP [_ /eqP->]. +case/orP=> [/eqP -> /eqP|hy]. + by rewrite exp0rz ?(negPf n0) expfz_eq0=> /andP [_ /eqP]. +move=> /(f_equal ( *%R^~ (y ^ (- n)))) /eqP. +rewrite -expfzDr ?(ltr_eqF hy) // subrr expr0z -exprz_inv -expfzMl. +rewrite pexprz_eq1 ?(negPf n0) /= ?mulr_le0 ?invr_le0 ?ltrW //. +by rewrite (can2_eq (mulrVK _) (mulrK _)) ?unitfE ?(ltr_eqF hy) // mul1r=> /eqP. +Qed. + +Lemma ler_pexpz2r n (hn : 0 < n) : + {in >= 0 & , {mono ((@exprz R)^~ n) : x y / x <= y}}. +Proof. +apply: homo_mono_in (homo_inj_in_lt _ _). + by move=> x y hx hy /=; apply: pexpIrz; rewrite // gtr_eqF. +by apply: ler_wpexpz2r; rewrite ltrW. +Qed. + +Lemma ltr_pexpz2r n (hn : 0 < n) : + {in >= 0 & , {mono ((@exprz R)^~ n) : x y / x < y}}. +Proof. exact: lerW_mono_in (ler_pexpz2r _). Qed. + +Lemma ler_nexpz2r n (hn : n < 0) : + {in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x <= y}}. +Proof. +apply: nhomo_mono_in (nhomo_inj_in_lt _ _); last first. + by apply: ler_wnexpz2r; rewrite ltrW. +by move=> x y hx hy /=; apply: pexpIrz; rewrite ?[_ \in _]ltrW ?ltr_eqF. +Qed. + +Lemma ltr_nexpz2r n (hn : n < 0) : + {in > 0 & , {mono ((@exprz R)^~ n) : x y /~ x < y}}. +Proof. exact: lerW_nmono_in (ler_nexpz2r _). Qed. + +Lemma eqr_expz2 n x y : n != 0 -> 0 <= x -> 0 <= y -> + (x ^ n == y ^ n) = (x == y). +Proof. by move=> *; rewrite (inj_in_eq (pexpIrz _)). Qed. + +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). +Proof. by rewrite /sgz; case: (_ == _); case: (_ < _). Qed. + +Lemma sgrEz x : sgr x = (sgz x)%:~R. Proof. by rewrite !(fun_if intr). Qed. + +Lemma gtr0_sgz x : 0 < x -> sgz x = 1. +Proof. by move=> x_gt0; rewrite /sgz ltr_neqAle andbC eqr_le ltr_geF //. Qed. + +Lemma ltr0_sgz x : x < 0 -> sgz x = -1. +Proof. by move=> x_lt0; rewrite /sgz eq_sym eqr_le x_lt0 ltr_geF. Qed. + +Lemma sgz0 : sgz (0 : R) = 0. Proof. by rewrite /sgz eqxx. Qed. +Lemma sgz1 : sgz (1 : R) = 1. Proof. by rewrite gtr0_sgz // ltr01. Qed. +Lemma sgzN1 : sgz (-1 : R) = -1. Proof. by rewrite ltr0_sgz // ltrN10. Qed. + +Definition sgzE := (sgz0, sgz1, sgzN1). + +Lemma sgz_sgr x : sgz (sgr x) = sgz x. +Proof. by rewrite !(fun_if sgz) !sgzE. Qed. + +Lemma normr_sgz x : `|sgz x| = (x != 0). +Proof. by rewrite sgz_def -mulr_natr normrMsign normr_nat natz. Qed. + +Lemma normr_sg x : `|sgr x| = (x != 0)%:~R. +Proof. by rewrite sgr_def -mulr_natr normrMsign normr_nat. Qed. + +End Sgz. + +Section MoreSgz. + +Variable R : numDomainType. + +Lemma sgz_int m : sgz (m%:~R : R) = sgz m. +Proof. by rewrite /sgz intr_eq0 ltrz0. Qed. + +Lemma sgrz (n : int) : sgr n = sgz n. Proof. by rewrite sgrEz intz. Qed. + +Lemma intr_sg m : (sgr m)%:~R = sgr (m%:~R) :> R. +Proof. by rewrite sgrz -sgz_int -sgrEz. Qed. + +Lemma sgz_id (x : R) : sgz (sgz x) = sgz x. +Proof. by rewrite !(fun_if (@sgz _)). Qed. + +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)). +Proof. by rewrite /sgz; case: ltrgtP. Qed. + +CoInductive sgz_val x : bool -> bool -> bool -> bool -> bool -> bool + -> bool -> bool -> bool -> bool -> bool -> bool + -> bool -> bool -> bool -> bool -> bool -> bool + -> R -> R -> int -> Set := + | SgzNull of x = 0 : sgz_val x true true true true false false + true false false true false false true false false true false false 0 0 0 + | SgzPos of x > 0 : sgz_val x false false true false false true + false false true false false true false false true false false true x 1 1 + | SgzNeg of x < 0 : sgz_val x false true false false true false + false true false false true false false true false false true false (-x) (-1) (-1). + +Lemma sgzP x : + sgz_val x (0 == x) (x <= 0) (0 <= x) (x == 0) (x < 0) (0 < x) + (0 == sgr x) (-1 == sgr x) (1 == sgr x) + (sgr x == 0) (sgr x == -1) (sgr x == 1) + (0 == sgz x) (-1 == sgz x) (1 == sgz x) + (sgz x == 0) (sgz x == -1) (sgz x == 1) `|x| (sgr x) (sgz x). +Proof. +rewrite ![_ == sgz _]eq_sym ![_ == sgr _]eq_sym !sgr_cp0 !sgz_cp0. +by rewrite /sgr /sgz !lerNgt; case: ltrgt0P; constructor. +Qed. + +Lemma sgzN x : sgz (- x) = - sgz x. +Proof. by rewrite /sgz oppr_eq0 oppr_lt0; case: ltrgtP. Qed. + +Lemma mulz_sg x : sgz x * sgz x = (x != 0)%:~R. +Proof. by case: sgzP; rewrite ?(mulr0, mulr1, mulrNN). Qed. + +Lemma mulz_sg_eq1 x y : (sgz x * sgz y == 1) = (x != 0) && (sgz x == sgz y). +Proof. +do 2?case: sgzP=> _; rewrite ?(mulr0, mulr1, mulrN1, opprK, oppr0, eqxx); + by rewrite ?[0 == 1]eq_sym ?oner_eq0 //= eqr_oppLR oppr0 oner_eq0. +Qed. + +Lemma mulz_sg_eqN1 x y : (sgz x * sgz y == -1) = (x != 0) && (sgz x == - sgz y). +Proof. by rewrite -eqr_oppLR -mulrN -sgzN mulz_sg_eq1. Qed. + +(* 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. +Proof. +case: (sgzP x)=> hx; first by rewrite hx ?mul0r sgz0. + case: (sgzP y)=> hy; first by rewrite hy !mulr0 sgz0. + by apply/eqP; rewrite mul1r sgz_cp0 pmulr_rgt0. + by apply/eqP; rewrite mul1r sgz_cp0 nmulr_llt0. +case: (sgzP y)=> hy; first by rewrite hy !mulr0 sgz0. + by apply/eqP; rewrite mulr1 sgz_cp0 nmulr_rlt0. +by apply/eqP; rewrite mulN1r opprK sgz_cp0 nmulr_rgt0. +Qed. + +Lemma sgzX (n : nat) x : sgz (x ^+ n) = (sgz x) ^+ n. +Proof. by elim: n => [|n IHn]; rewrite ?sgz1 // !exprS sgzM IHn. Qed. + +Lemma sgz_eq0 x : (sgz x == 0) = (x == 0). +Proof. by rewrite sgz_cp0. Qed. + +Lemma sgz_odd (n : nat) x : x != 0 -> (sgz x) ^+ n = (sgz x) ^+ (odd n). +Proof. by case: sgzP => //=; rewrite ?expr1n // signr_odd. Qed. + +Lemma sgz_gt0 x : (sgz x > 0) = (x > 0). +Proof. by case: sgzP. Qed. + +Lemma sgz_lt0 x : (sgz x < 0) = (x < 0). +Proof. by case: sgzP. Qed. + +Lemma sgz_ge0 x : (sgz x >= 0) = (x >= 0). +Proof. by case: sgzP. Qed. + +Lemma sgz_le0 x : (sgz x <= 0) = (x <= 0). +Proof. by case: sgzP. Qed. + +Lemma sgz_smul x y : sgz (y *~ (sgz x)) = (sgz x) * (sgz y). +Proof. by rewrite -mulrzl sgzM -sgrEz sgz_sgr. Qed. + +Lemma sgrMz m x : sgr (x *~ m) = sgr x *~ sgr m. +Proof. by rewrite -mulrzr sgrM -intr_sg mulrzr. Qed. + +End SgzReal. + +Lemma sgz_eq (R R' : realDomainType) (x : R) (y : R') : + (sgz x == sgz y) = ((x == 0) == (y == 0)) && ((0 < x) == (0 < y)). +Proof. by do 2!case: sgzP. Qed. + +Lemma intr_sign (R : ringType) s : ((-1) ^+ s)%:~R = (-1) ^+ s :> R. +Proof. exact: rmorph_sign. Qed. + +Section Absz. + +Implicit Types m n p : int. +Open Scope nat_scope. +Local Coercion Posz : nat >-> int. + +Lemma absz_nat (n : nat) : `|n| = n. Proof. by []. Qed. + +Lemma abszE (m : int) : `|m| = `|m|%R :> int. Proof. by []. Qed. + +Lemma absz0 : `|0%R| = 0. Proof. by []. Qed. + +Lemma abszN m : `|- m| = `|m|. Proof. by case: (normrN m). Qed. + +Lemma absz_eq0 m : (`|m| == 0) = (m == 0%R). Proof. by case: (intP m). Qed. + +Lemma absz_gt0 m : (`|m| > 0) = (m != 0%R). Proof. by case: (intP m). Qed. + +Lemma absz1 : `|1%R| = 1. Proof. by []. Qed. + +Lemma abszN1 : `|-1%R| = 1. Proof. by []. Qed. + +Lemma absz_id m : `|(`|m|)| = `|m|. Proof. by []. Qed. + +Lemma abszM m1 m2 : `|(m1 * m2)%R| = `|m1| * `|m2|. +Proof. by case: m1 m2 => [[|m1]|m1] [[|m2]|m2]; rewrite //= mulnS mulnC. Qed. + +Lemma abszX (n : nat) m : `|m ^+ n| = `|m| ^ n. +Proof. by elim: n => // n ihn; rewrite exprS expnS abszM ihn. Qed. + +Lemma absz_sg m : `|sgr m| = (m != 0%R). Proof. by case: (intP m). Qed. + +Lemma gez0_abs m : (0 <= m)%R -> `|m| = m :> int. +Proof. by case: (intP m). Qed. + +Lemma gtz0_abs m : (0 < m)%R -> `|m| = m :> int. +Proof. by case: (intP m). Qed. + +Lemma lez0_abs m : (m <= 0)%R -> `|m| = - m :> int. +Proof. by case: (intP m). Qed. + +Lemma ltz0_abs m : (m < 0)%R -> `|m| = - m :> int. +Proof. by case: (intP m). Qed. + +Lemma absz_sign s : `|(-1) ^+ s| = 1. +Proof. by rewrite abszX exp1n. Qed. + +Lemma abszMsign s m : `|((-1) ^+ s * m)%R| = `|m|. +Proof. by rewrite abszM absz_sign mul1n. Qed. + +Lemma mulz_sign_abs m : ((-1) ^+ (m < 0)%R * `|m|%:Z)%R = m. +Proof. by rewrite abszE mulr_sign_norm. Qed. + +Lemma mulz_Nsign_abs m : ((-1) ^+ (0 < m)%R * `|m|%:Z)%R = - m. +Proof. by rewrite abszE mulr_Nsign_norm. Qed. + +Lemma intEsign m : m = ((-1) ^+ (m < 0)%R * `|m|%:Z)%R. +Proof. exact: numEsign. Qed. + +Lemma abszEsign m : `|m|%:Z = ((-1) ^+ (m < 0)%R * m)%R. +Proof. exact: normrEsign. Qed. + +Lemma intEsg m : m = (sgz m * `|m|%:Z)%R. +Proof. by rewrite -sgrz -numEsg. Qed. + +Lemma abszEsg m : (`|m|%:Z = sgz m * m)%R. +Proof. by rewrite -sgrz -normrEsg. Qed. + +End Absz. + +Module Export IntDist. + +Notation "m - n" := + (@GRing.add int_ZmodType m%N (@GRing.opp int_ZmodType n%N)) : distn_scope. +Arguments Scope absz [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|. +Proof. by rewrite -opprB abszN. Qed. + +Lemma distnDl d n1 n2 : `|d + n1 - (d + n2)| = `|n1 - n2|. +Proof. by rewrite !PoszD opprD addrCA -addrA addKr. Qed. + +Lemma distnDr d n1 n2 : `|n1 + d - (n2 + d)| = `|n1 - n2|. +Proof. by rewrite -!(addnC d) distnDl. Qed. + +Lemma distnEr n1 n2 : n1 <= n2 -> `|n1 - n2| = n2 - n1. +Proof. by move/subnK=> {1}<-; rewrite distnC PoszD addrK absz_nat. Qed. + +Lemma distnEl n1 n2 : n2 <= n1 -> `|n1 - n2| = n1 - n2. +Proof. by move/distnEr <-; rewrite distnC. Qed. + +Lemma distn0 n : `|n - 0| = n. +Proof. by rewrite subr0 absz_nat. Qed. + +Lemma dist0n n : `|0 - n| = n. +Proof. by rewrite distnC distn0. Qed. + +Lemma distnn m : `|m - m| = 0. +Proof. by rewrite subrr. Qed. + +Lemma distn_eq0 n1 n2 : (`|n1 - n2| == 0) = (n1 == n2). +Proof. by rewrite absz_eq0 subr_eq0. Qed. + +Lemma distnS n : `|n - n.+1| = 1. +Proof. exact: distnDr n 0 1. Qed. + +Lemma distSn n : `|n.+1 - n| = 1. +Proof. exact: distnDr n 1 0. Qed. + +Lemma distn_eq1 n1 n2 : + (`|n1 - n2| == 1) = (if n1 < n2 then n1.+1 == n2 else n1 == n2.+1). +Proof. +case: ltnP => [lt_n12 | le_n21]. + by rewrite eq_sym -(eqn_add2r n1) distnEr ?subnK // ltnW. +by rewrite -(eqn_add2r n2) distnEl ?subnK. +Qed. + +Lemma leq_add_dist m1 m2 m3 : `|m1 - m3| <= `|m1 - m2| + `|m2 - m3|. +Proof. by rewrite -lez_nat PoszD !abszE ler_dist_add. Qed. + +(* 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. +Proof. +apply/leqifP; rewrite -ltz_nat -eqz_nat PoszD !abszE; apply/lerifP. +wlog le_m31 : m1 m3 / (m3 <= m1)%R. + move=> IH; case/orP: (ler_total m1 m3) => /IH //. + by rewrite (addrC `|_|)%R orbC !(distrC m1) !(distrC m3). +rewrite ger0_norm ?subr_ge0 // orb_idl => [|/andP[le_m12 le_m23]]; last first. + by have /eqP->: m2 == m3; rewrite ?lerr // eqr_le le_m23 (ler_trans le_m31). +rewrite -{1}(subrK m2 m1) -addrA -subr_ge0 andbC -subr_ge0. +by apply: lerif_add; apply/real_lerif_norm/num_real. +Qed. + +Lemma leqif_add_dist n1 n2 n3 : + `|n1 - n3| <= `|n1 - n2| + `|n2 - n3| + ?= iff (n1 <= n2 <= n3) || (n3 <= n2 <= n1). +Proof. exact: leqif_add_distz. Qed. + +Lemma sqrn_dist n1 n2 : `|n1 - n2| ^ 2 + 2 * (n1 * n2) = n1 ^ 2 + n2 ^ 2. +Proof. +wlog le_n21: n1 n2 / n2 <= n1. + move=> IH; case/orP: (leq_total n2 n1) => /IH //. + by rewrite (addnC (n2 ^ 2)) (mulnC n2) distnC. +by rewrite distnEl ?sqrn_sub ?subnK ?nat_Cauchy. +Qed. + +End Distn. + +End IntDist. + +Section NormInt. + +Variable R : numDomainType. + +Lemma intr_norm m : `|m|%:~R = `|m%:~R| :> R. +Proof. by rewrite {2}[m]intEsign rmorphMsign normrMsign abszE normr_nat. Qed. + +Lemma normrMz m (x : R) : `|x *~ m| = `|x| *~ `|m|. +Proof. by rewrite -mulrzl normrM -intr_norm mulrzl. Qed. + +Lemma expN1r (i : int) : (-1 : R) ^ i = (-1) ^+ `|i|. +Proof. +case: i => n; first by rewrite exprnP absz_nat. +by rewrite NegzE abszN absz_nat -invr_expz expfV invrN1. +Qed. + +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 : forall p n i, (p *~ n)`_i = (p`_i *~ n). +Proof. by move=> p [] n i; rewrite ?NegzE (coefMNn, coefMn). Qed. + +Lemma polyC_mulrz : forall n, {morph (@polyC R) : c / c *~ n}. +Proof. +move=> [] n c; rewrite ?NegzE -?pmulrn ?polyC_muln //. +by rewrite polyC_opp mulrNz polyC_muln nmulrn. +Qed. + +Lemma hornerMz : forall n (p : {poly R}) x, (p *~ n).[x] = p.[x] *~ n. +Proof. by case=> *; rewrite ?NegzE ?mulNzr ?(hornerN, hornerMn). Qed. + +Lemma horner_int : forall n x, (n%:~R : {poly R}).[x] = n%:~R. +Proof. by move=> n x; rewrite hornerMz hornerC. Qed. + +Lemma derivMz : forall n p, (p *~ n)^`() = p^`() *~ n. +Proof. by move=> [] n p; rewrite ?NegzE -?pmulrn (derivMn, derivMNn). Qed. + +End PolyZintRing. + +Section PolyZintOIdom. + +Variable R : realDomainType. + +Lemma mulpz (p : {poly R}) (n : int) : p *~ n = n%:~R *: p. +Proof. by rewrite -[p *~ n]mulrzl -mul_polyC polyC_mulrz polyC1. Qed. + +End PolyZintOIdom. + +Section ZnatPred. + +Definition Znat := [qualify a n : int | 0 <= n]. +Fact Znat_key : pred_key Znat. by []. Qed. +Canonical Znat_keyd := KeyedQualifier Znat_key. + +Lemma Znat_def n : (n \is a Znat) = (0 <= n). Proof. by []. Qed. + +Lemma Znat_semiring_closed : semiring_closed Znat. +Proof. by do 2?split => //; [exact: addr_ge0 | exact: mulr_ge0]. Qed. +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 (exists n : nat, m = n) (m \is a Znat). +Proof. by apply: (iffP idP) => [|[n -> //]]; case: m => // n; exists n. Qed. + +End ZnatPred. + +Section rpred. + +Lemma rpredMz M S (addS : @zmodPred M S) (kS : keyed_pred addS) m : + {in kS, forall u, u *~ m \in kS}. +Proof. by case: m => n u Su; rewrite ?rpredN ?rpredMn. Qed. + +Lemma rpred_int R S (ringS : @subringPred R S) (kS : keyed_pred ringS) m : + m%:~R \in kS. +Proof. by rewrite rpredMz ?rpred1. Qed. + +Lemma rpredZint (R : ringType) (M : lmodType R) S + (addS : @zmodPred M S) (kS : keyed_pred addS) m : + {in kS, forall u, m%:~R *: u \in kS}. +Proof. by move=> u Su; rewrite /= scaler_int rpredMz. Qed. + +Lemma rpredXz R S (divS : @divrPred R S) (kS : keyed_pred divS) m : + {in kS, forall x, x ^ m \in kS}. +Proof. by case: m => n x Sx; rewrite ?rpredV rpredX. Qed. + +Lemma rpredXsign R S (divS : @divrPred R S) (kS : keyed_pred divS) n x : + (x ^ ((-1) ^+ n) \in kS) = (x \in kS). +Proof. by rewrite -signr_odd; case: (odd n); rewrite ?rpredV. Qed. + +End rpred.
\ No newline at end of file |