Library mathcomp.analysis.constructive_ereal

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              
 -------------------------------------------------------------------- 
 Copyright (c) - 2015--2016 - IMDEA Software Institute                
 Copyright (c) - 2015--2018 - Inria                                   
 Copyright (c) - 2016--2018 - Polytechnique                           
 -------------------------------------------------------------------- *)

From mathcomp Require Import all_ssreflect all_algebra finmap.
From mathcomp Require Import mathcomp_extra.
Require Import signed.

Set Implicit Arguments.

Reserved Notation "x %:E" (at level 2, format "x %:E").
Reserved Notation "x +? y" (at level 50, format "x +? y").
Reserved Notation "x *? y" (at level 50, format "x *? y").
Reserved Notation "'\bar' x" (at level 2, format "'\bar' x").
Reserved Notation "{ 'posnum' '\bar' R }" (at level 0,
  format "{ 'posnum' '\bar' R }").
Reserved Notation "{ 'nonneg' '\bar' R }" (at level 0,
  format "{ 'nonneg' '\bar' R }").

Declare Scope ereal_dual_scope.
Declare Scope ereal_scope.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope ring_scope.

Variant extended (R : Type) := EFin of R | EPInf | ENInf.
Arguments EFin {R}.

Lemma EFin_inj T : injective (@EFin T).

Definition dual_extended := extended.

Notation "+oo" := (@EPInf _ : dual_extended _) : ereal_dual_scope.
Notation "+oo" := (@EPInf _) : ereal_scope.
Notation "-oo" := (@ENInf _ : dual_extended _) : ereal_dual_scope.
Notation "-oo" := (@ENInf _) : ereal_scope.
Notation "r %:E" := (@EFin _ r%R).
Notation "'\bar' R" := (extended R) : type_scope.
Notation "0" := (0%R%:E : dual_extended _) : ereal_dual_scope.
Notation "0" := (0%R%:E) : ereal_scope.
Notation "1" := (1%R%:E : dual_extended _) : ereal_dual_scope.
Notation "1" := (1%R%:E) : ereal_scope.

Bind Scope ereal_dual_scope with dual_extended.
Bind Scope ereal_scope with extended.
Delimit Scope ereal_dual_scope with dE.
Delimit Scope ereal_scope with E.

Local Open Scope ereal_scope.

Definition er_map T T' (f : T → T') (x : \bar T) : \bar T' :=
  match x with
  | r%:E ⇒ (f r)%:E
  | +oo ⇒ +oo
  | -oo ⇒ -oo
  end.

Lemma er_map_idfun T (x : \bar T) : er_map idfun x = x.

Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.

Section EqEReal.
Variable (R : eqType).

Definition eq_ereal (x y : \bar R) :=
  match x, y with
    | x%:E, y%:E ⇒ x == y
    | +oo, +oo ⇒ true
    | -oo, -oo ⇒ true
    | _, _ ⇒ false
  end.

Lemma ereal_eqP : Equality.axiom eq_ereal.

Definition ereal_eqMixin := Equality.Mixin ereal_eqP.
Canonical ereal_eqType := Equality.Pack ereal_eqMixin.

Lemma eqe (r1 r2 : R) : (r1%:E == r2%:E) = (r1 == r2).

End EqEReal.

Section ERealChoice.
Variable (R : choiceType).

Definition code (x : \bar R) :=
  match x with
  | r%:E ⇒ GenTree.Node 0 [:: GenTree.Leaf r]
  | +oo ⇒ GenTree.Node 1 [::]
  | -oo ⇒ GenTree.Node 2 [::]
  end.

Definition decode (x : GenTree.tree R) : option (\bar R) :=
  match x with
  | GenTree.Node 0 [:: GenTree.Leaf r] ⇒ Some r%:E
  | GenTree.Node 1 [::] ⇒ Some +oo
  | GenTree.Node 2 [::] ⇒ Some -oo
  | _ ⇒ None
  end.

Lemma codeK : pcancel code decode.

Definition ereal_choiceMixin := PcanChoiceMixin codeK.
Canonical ereal_choiceType := ChoiceType (extended R) ereal_choiceMixin.

End ERealChoice.

Section ERealCount.
Variable (R : countType).

Definition ereal_countMixin := PcanCountMixin (@codeK R).
Canonical ereal_countType := CountType (extended R) ereal_countMixin.

End ERealCount.

Section ERealOrder.
Context {R : numDomainType}.
Implicit Types x y : \bar R.

Definition le_ereal x1 x2 :=
  match x1, x2 with
  | -oo, r%:E | r%:E, +oo ⇒ r \is Num.real
  | r1%:E, r2%:E ⇒ r1 ≤ r2
  | -oo, _ | _, +oo ⇒ true
  | +oo, _ | _, -oo ⇒ false
  end.

Definition lt_ereal x1 x2 :=
  match x1, x2 with
  | -oo, r%:E | r%:E, +oo ⇒ r \is Num.real
  | r1%:E, r2%:E ⇒ r1 < r2
  | -oo, -oo | +oo, +oo ⇒ false
  | +oo, _ | _ , -oo ⇒ false
  | -oo, _ ⇒ true
  end.

Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.

Lemma le_refl_ereal : reflexive le_ereal.

Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.

Lemma le_trans_ereal : ssrbool.transitive le_ereal.

Fact ereal_display : unit.

Definition ereal_porderMixin :=
  LePOrderMixin lt_def_ereal le_refl_ereal le_anti_ereal le_trans_ereal.

Canonical ereal_porderType :=
  POrderType ereal_display (extended R) ereal_porderMixin.

Lemma leEereal x y : (x ≤ y)%O = le_ereal x y.
Lemma ltEereal x y : (x < y)%O = lt_ereal x y.

End ERealOrder.

Notation lee := (@Order.le ereal_display _) (only parsing).
Notation "@ 'lee' R" :=
  (@Order.le ereal_display R) (at level 10, R at level 8, only parsing).
Notation lte := (@Order.lt ereal_display _) (only parsing).
Notation "@ 'lte' R" :=
  (@Order.lt ereal_display R) (at level 10, R at level 8, only parsing).
Notation gee := (@Order.ge ereal_display _) (only parsing).
Notation "@ 'gee' R" :=
  (@Order.ge ereal_display R) (at level 10, R at level 8, only parsing).
Notation gte := (@Order.gt ereal_display _) (only parsing).
Notation "@ 'gte' R" :=
  (@Order.gt ereal_display R) (at level 10, R at level 8, only parsing).

Notation "x <= y" := (lee x y) (only printing) : ereal_dual_scope.
Notation "x <= y" := (lee x y) (only printing) : ereal_scope.
Notation "x < y" := (lte x y) (only printing) : ereal_dual_scope.
Notation "x < y" := (lte x y) (only printing) : ereal_scope.

Notation "x <= y <= z" := ((lee x y) && (lee y z)) (only printing) : ereal_dual_scope.
Notation "x <= y <= z" := ((lee x y) && (lee y z)) (only printing) : ereal_scope.
Notation "x < y <= z" := ((lte x y) && (lee y z)) (only printing) : ereal_dual_scope.
Notation "x < y <= z" := ((lte x y) && (lee y z)) (only printing) : ereal_scope.
Notation "x <= y < z" := ((lee x y) && (lte y z)) (only printing) : ereal_dual_scope.
Notation "x <= y < z" := ((lee x y) && (lte y z)) (only printing) : ereal_scope.
Notation "x < y < z" := ((lte x y) && (lte y z)) (only printing) : ereal_dual_scope.
Notation "x < y < z" := ((lte x y) && (lte y z)) (only printing) : ereal_scope.

Notation "x <= y" := (lee (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x <= y" := (lee (x : extended _) (y : extended _)) : ereal_scope.
Notation "x < y" := (lte (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x < y" := (lte (x : extended _) (y : extended _)) : ereal_scope.
Notation "x >= y" := (y ≤ x) (only parsing) : ereal_dual_scope.
Notation "x >= y" := (y ≤ x) (only parsing) : ereal_scope.
Notation "x > y" := (y < x) (only parsing) : ereal_dual_scope.
Notation "x > y" := (y < x) (only parsing) : ereal_scope.

Notation "x <= y <= z" := ((x ≤ y) && (y ≤ z)) : ereal_dual_scope.
Notation "x <= y <= z" := ((x ≤ y) && (y ≤ z)) : ereal_scope.
Notation "x < y <= z" := ((x < y) && (y ≤ z)) : ereal_dual_scope.
Notation "x < y <= z" := ((x < y) && (y ≤ z)) : ereal_scope.
Notation "x <= y < z" := ((x ≤ y) && (y < z)) : ereal_dual_scope.
Notation "x <= y < z" := ((x ≤ y) && (y < z)) : ereal_scope.
Notation "x < y < z" := ((x < y) && (y < z)) : ereal_dual_scope.
Notation "x < y < z" := ((x < y) && (y < z)) : ereal_scope.

Notation "x <= y :> T" := ((x : T) ≤ (y : T)) (only parsing) : ereal_scope.
Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : ereal_scope.

Section ERealOrder_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y : \bar R) (r : R).

Lemma lee_fin (r s : R) : (r%:E ≤ s%:E) = (r ≤ s)%R.

Lemma lte_fin (r s : R) : (r%:E < s%:E) = (r < s)%R.

Lemma lee01 : 0 ≤ 1 :> \bar R.

Lemma lte01 : 0 < 1 :> \bar R.

Lemma leeNy_eq x : (x ≤ -oo) = (x == -oo).

Lemma leye_eq x : (+oo ≤ x) = (x == +oo).

Lemma lt0y : (0 : \bar R) < +oo.

Lemma ltNy0 : -oo < (0 : \bar R).

Lemma le0y : (0 : \bar R) ≤ +oo.

Lemma leNy0 : -oo ≤ (0 : \bar R).

Lemma lt0e x : (0 < x) = (x != 0) && (0 ≤ x).

Lemma ereal_comparable x y : (0%E >=< x)%O → (0%E >=< y)%O → (x >=< y)%O.

Lemma real_ltry r : r%:E < +oo = (r \is Num.real).
Lemma real_ltNyr r : -oo < r%:E = (r \is Num.real).

Lemma real_leey x : (x ≤ +oo) = (fine x \is Num.real).

Lemma real_leNye x : (-oo ≤ x) = (fine x \is Num.real).

Lemma gee0P x : 0 ≤ x ↔ x = +oo ∨ exists2 r, (r ≥ 0)%R & x = r%:E.

Lemma fine0 : fine 0 = 0%R :> R.
Lemma fine1 : fine 1 = 1%R :> R.

End ERealOrder_numDomainType.

#[global] Hint Resolve lee01 lte01 : core.

Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).

Lemma ltry r : r%:E < +oo.

Lemma ltey x : (x < +oo) = (x != +oo).

Lemma ltNyr r : -oo < r%:E.

Lemma ltNye x : (-oo < x) = (x != -oo).

Lemma leey x : x ≤ +oo.

Lemma leNye x : -oo ≤ x.

Definition lteey := (ltey, leey).

Definition lteNye := (ltNye, leNye).

Lemma le_er_map (f : R → R) : {homo f : x y / (x ≤ y)%R} →
  {homo er_map f : x y / x ≤ y}.

Lemma le_total_ereal : totalPOrderMixin [porderType of \bar R].

Canonical ereal_latticeType := LatticeType (extended R) le_total_ereal.
Canonical ereal_distrLatticeType := DistrLatticeType (extended R) le_total_ereal.
Canonical ereal_orderType := OrderType (extended R) le_total_ereal.

Lemma ereal_blatticeMixin :
  Order.BLattice.mixin_of (Order.POrder.class (@ereal_porderType R)).
Canonical ereal_blatticeType := BLatticeType (extended R) ereal_blatticeMixin.

Lemma ereal_tblatticeMixin :
  Order.TBLattice.mixin_of (Order.POrder.class ereal_blatticeType).
Canonical ereal_tblatticeType := TBLatticeType (extended R) ereal_tblatticeMixin.

End ERealOrder_realDomainType.

Section ERealArith.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.

Definition adde_subdef x y :=
  match x, y with
  | x%:E , y%:E ⇒ (x + y)%:E
  | -oo, _ ⇒ -oo
  | _ , -oo ⇒ -oo
  | +oo, _ ⇒ +oo
  | _ , +oo ⇒ +oo
  end.

Definition adde := nosimpl adde_subdef.

Definition dual_adde_subdef x y :=
  match x, y with
  | x%:E , y%:E ⇒ (x + y)%R%:E
  | +oo, _ ⇒ +oo
  | _ , +oo ⇒ +oo
  | -oo, _ ⇒ -oo
  | _ , -oo ⇒ -oo
  end.

Definition dual_adde := nosimpl dual_adde_subdef.

Definition oppe x :=
  match x with
  | r%:E ⇒ (- r)%:E
  | -oo ⇒ +oo
  | +oo ⇒ -oo
  end.

Definition mule_subdef x y :=
  match x, y with
  | x%:E , y%:E ⇒ (x × y)%:E
  | -oo, y | y, -oo ⇒ if y == 0 then 0 else if 0 < y then -oo else +oo
  | +oo, y | y, +oo ⇒ if y == 0 then 0 else if 0 < y then +oo else -oo
  end.

Definition mule := nosimpl mule_subdef.

Definition abse x := if x is r%:E then `|r|%:E else +oo.

Definition expe x n := iterop n mule x 1.

Definition enatmul x n := iterop n adde x 0.

Definition ednatmul x n := iterop n dual_adde x 0.

End ERealArith.

Notation "+%dE" := dual_adde.
Notation "+%E" := adde.
Notation "-%E" := oppe.
Notation "x + y" := (dual_adde x%dE y%dE) : ereal_dual_scope.
Notation "x + y" := (adde x y) : ereal_scope.
Notation "x - y" := (dual_adde x%dE (oppe y%dE)) : ereal_dual_scope.
Notation "x - y" := (adde x (oppe y)) : ereal_scope.
Notation "- x" := (oppe (x%dE : dual_extended _)) : ereal_dual_scope.
Notation "- x" := (oppe x) : ereal_scope.
Notation "*%E" := mule.
Notation "x * y" := (mule (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x * y" := (mule x y) : ereal_scope.
Notation "`| x |" := (abse (x%dE : dual_extended _)) : ereal_dual_scope.
Notation "`| x |" := (abse x) : ereal_scope.
Arguments abse {R}.
Notation "x ^+ n" := (expe x%dE n) : ereal_dual_scope.
Notation "x ^+ n" := (expe x n) : ereal_scope.
Notation "x *+ n" := (ednatmul x%dE n) : ereal_dual_scope.
Notation "x *+ n" := (enatmul x n) : ereal_scope.

Notation "\- f" := (fun x ⇒ - f x)%dE : ereal_dual_scope.
Notation "\- f" := (fun x ⇒ - f x)%E : ereal_scope.
Notation "f \+ g" := (fun x ⇒ f x + g x)%dE : ereal_dual_scope.
Notation "f \+ g" := (fun x ⇒ f x + g x)%E : ereal_scope.
Notation "f \* g" := (fun x ⇒ f x × g x)%dE : ereal_dual_scope.
Notation "f \* g" := (fun x ⇒ f x × g x)%E : ereal_scope.
Notation "f \- g" := (fun x ⇒ f x - g x)%dE : ereal_dual_scope.
Notation "f \- g" := (fun x ⇒ f x - g x)%E : ereal_scope.

Notation "\sum_ ( i <- r | P ) F" :=
  (\big[+%dE/0%:E]_(i <- r | P%B) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i <- r | P ) F" :=
  (\big[+%E/0%:E]_(i <- r | P%B) F%E) : ereal_scope.
Notation "\sum_ ( i <- r ) F" :=
  (\big[+%dE/0%:E]_(i <- r) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i <- r ) F" :=
  (\big[+%E/0%:E]_(i <- r) F%E) : ereal_scope.
Notation "\sum_ ( m <= i < n | P ) F" :=
  (\big[+%dE/0%:E]_(m ≤ i < n | P%B) F%dE) : ereal_dual_scope.
Notation "\sum_ ( m <= i < n | P ) F" :=
  (\big[+%E/0%:E]_(m ≤ i < n | P%B) F%E) : ereal_scope.
Notation "\sum_ ( m <= i < n ) F" :=
  (\big[+%dE/0%:E]_(m ≤ i < n) F%dE) : ereal_dual_scope.
Notation "\sum_ ( m <= i < n ) F" :=
  (\big[+%E/0%:E]_(m ≤ i < n) F%E) : ereal_scope.
Notation "\sum_ ( i | P ) F" :=
  (\big[+%dE/0%:E]_(i | P%B) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i | P ) F" :=
  (\big[+%E/0%:E]_(i | P%B) F%E) : ereal_scope.
Notation "\sum_ i F" :=
  (\big[+%dE/0%:E]_i F%dE) : ereal_dual_scope.
Notation "\sum_ i F" :=
  (\big[+%E/0%:E]_i F%E) : ereal_scope.
Notation "\sum_ ( i : t | P ) F" :=
  (\big[+%dE/0%:E]_(i : t | P%B) F%dE) (only parsing) : ereal_dual_scope.
Notation "\sum_ ( i : t | P ) F" :=
  (\big[+%E/0%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope.
Notation "\sum_ ( i : t ) F" :=
  (\big[+%dE/0%:E]_(i : t) F%dE) (only parsing) : ereal_dual_scope.
Notation "\sum_ ( i : t ) F" :=
  (\big[+%E/0%:E]_(i : t) F%E) (only parsing) : ereal_scope.
Notation "\sum_ ( i < n | P ) F" :=
  (\big[+%dE/0%:E]_(i < n | P%B) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i < n | P ) F" :=
  (\big[+%E/0%:E]_(i < n | P%B) F%E) : ereal_scope.
Notation "\sum_ ( i < n ) F" :=
  (\big[+%dE/0%:E]_(i < n) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i < n ) F" :=
  (\big[+%E/0%:E]_(i < n) F%E) : ereal_scope.
Notation "\sum_ ( i 'in' A | P ) F" :=
  (\big[+%dE/0%:E]_(i in A | P%B) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i 'in' A | P ) F" :=
  (\big[+%E/0%:E]_(i in A | P%B) F%E) : ereal_scope.
Notation "\sum_ ( i 'in' A ) F" :=
  (\big[+%dE/0%:E]_(i in A) F%dE) : ereal_dual_scope.
Notation "\sum_ ( i 'in' A ) F" :=
  (\big[+%E/0%:E]_(i in A) F%E) : ereal_scope.

Section ERealOrderTheory.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.




Lemma lee0N1 : 0 ≤ (-1)%:E :> \bar R = false.

Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false.

Lemma lteN10 : - 1%E < 0 :> \bar R.

Lemma leeN10 : - 1%E ≤ 0 :> \bar R.

Lemma lte0n n : (0 < n%:R%:E :> \bar R) = (0 < n)%N.

Lemma lee0n n : (0 ≤ n%:R%:E :> \bar R) = (0 ≤ n)%N.

Lemma lte1n n : (1 < n%:R%:E :> \bar R) = (1 < n)%N.

Lemma lee1n n : (1 ≤ n%:R%:E :> \bar R) = (1 ≤ n)%N.

Lemma fine_ge0 x : 0 ≤ x → (0 ≤ fine x)%R.

Lemma fine_gt0 x : 0 < x < +oo → (0 < fine x)%R.

Lemma fine_lt0 x : -oo < x < 0 → (fine x < 0)%R.

Lemma fine_le0 x : x ≤ 0 → (fine x ≤ 0)%R.

Lemma lee_tofin (r0 r1 : R) : (r0 ≤ r1)%R → r0%:E ≤ r1%:E.

Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R → r0%:E < r1%:E.

Lemma enatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.

Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.

Lemma EFin_natmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.

Lemma mule2n x : x *+ 2 = x + x.

Lemma expe2 x : x ^+ 2 = x × x.

End ERealOrderTheory.
#[global] Hint Resolve leeN10 lteN10 : core.

Section finNumPred.
Context {R : numDomainType}.
Implicit Type (x : \bar R).

Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
Fact fin_num_key : pred_key fin_num.
Canonical fin_num_keyd := KeyedQualifier fin_num_key.

Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).

Lemma fin_numP x : reflect ((x != -oo) ∧ (x != +oo)) (x \is a fin_num).

Lemma fin_numEn x : (x \isn't a fin_num) = (x == -oo) || (x == +oo).

Lemma fin_numPn x : reflect (x = -oo ∨ x = +oo) (x \isn't a fin_num).

Lemma fin_real x : -oo < x < +oo → x \is a fin_num.

Lemma fin_num_abs x : (x \is a fin_num) = (`| x | < +oo)%E.

End finNumPred.

Section ERealArithTh_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y z : \bar R) (r : R).

Lemma fine_le : {in fin_num &, {homo @fine R : x y / x ≤ y >-> (x ≤ y)%R}}.

Lemma fine_lt : {in fin_num &, {homo @fine R : x y / x < y >-> (x < y)%R}}.

Lemma fine_abse : {in fin_num, {morph @fine R : x / `|x| >-> `|x|%R}}.

Lemma abse_fin_num x : (`|x| \is a fin_num) = (x \is a fin_num).

Lemma fine_eq0 x : x \is a fin_num → (fine x == 0%R) = (x == 0).

Lemma EFinN r : (- r)%:E = (- r%:E).

Lemma fineN x : fine (- x) = (- fine x)%R.

Lemma EFinD r r' : (r + r')%:E = r%:E + r'%:E.

Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E.

Lemma EFinM r r' : (r × r')%:E = r%:E × r'%:E.

Lemma sumEFin I s P (F : I → R) :
  \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.

Definition adde_def x y :=
  ~~ ((x == +oo) && (y == -oo)) && ~~ ((x == -oo) && (y == +oo)).


Lemma adde_defC x y : x +? y = y +? x.

Lemma fin_num_adde_defr x y : x \is a fin_num → x +? y.

Lemma fin_num_adde_defl x y : y \is a fin_num → x +? y.

Lemma adde_defN x y : x +? - y = - x +? y.

Lemma adde_defDr x y z : x +? y → x +? z → x +? (y + z).

Lemma adde_defEninfty x : (x +? -oo) = (x != +oo).

Lemma ge0_adde_def : {in [pred x | x ≥ 0] &, ∀ x y, x +? y}.

Lemma addeC : commutative (S := \bar R) +%E.

Lemma adde0 : right_id (0 : \bar R) +%E.

Lemma add0e : left_id (0 : \bar R) +%E.

Lemma addeA : associative (S := \bar R) +%E.

Canonical adde_monoid := Monoid.Law addeA add0e adde0.
Canonical adde_comoid := Monoid.ComLaw addeC.

Lemma adde_def_sum I h t (P : pred I) (f : I → \bar R) :
    {in P, ∀ i : I, f h +? f i} →
  f h +? \sum_(j <- t | P j) f j.

Lemma addeAC : @right_commutative (\bar R) _ +%E.

Lemma addeCA : @left_commutative (\bar R) _ +%E.

Lemma addeACA : @interchange (\bar R) +%E +%E.

Lemma adde_gt0 x y : 0 < x → 0 < y → 0 < x + y.

Lemma padde_eq0 x y : 0 ≤ x → 0 ≤ y → (x + y == 0) = (x == 0) && (y == 0).

Lemma nadde_eq0 x y : x ≤ 0 → y ≤ 0 → (x + y == 0) = (x == 0) && (y == 0).

Lemma realDe x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x + y)%O.

Lemma oppe0 : - 0 = 0 :> \bar R.

Lemma oppeK : involutive (A := \bar R) -%E.

Lemma oppe_inj : @injective (\bar R) _ -%E.

Lemma adde_defNN x y : - x +? - y = x +? y.

Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E.

Lemma oppeD x y : x +? y → - (x + y) = - x - y.

Lemma fin_num_oppeD x y : y \is a fin_num → - (x + y) = - x - y.

Lemma sube0 x : x - 0 = x.

Lemma sub0e x : 0 - x = - x.

Lemma muleC x y : x × y = y × x.

Lemma onee_neq0 : 1 != 0 :> \bar R.
Lemma onee_eq0 : 1 == 0 :> \bar R = false.

Lemma mule1 x : x × 1 = x.

Lemma mul1e x : 1 × x = x.

Lemma mule0 x : x × 0 = 0.

Lemma mul0e x : 0 × x = 0.

Canonical mule_mulmonoid := @Monoid.MulLaw _ _ mule mul0e mule0.

Lemma expeS x n : x ^+ n.+1 = x × x ^+ n.

Lemma EFin_expe r n : (r ^+ n)%:E = r%:E ^+ n.

Definition mule_def x y :=
  ~~ (((x == 0) && (`| y | == +oo)) || ((y == 0) && (`| x | == +oo))).


Lemma mule_defC x y : x *? y = y *? x.

Lemma mule_def_fin x y : x \is a fin_num → y \is a fin_num → x *? y.

Lemma mule_def_neq0_infty x y : x != 0 → y \isn't a fin_num → x *? y.

Lemma mule_def_infty_neq0 x y : x \isn't a fin_num → y!= 0 → x *? y.

Lemma neq0_mule_def x y : x × y != 0 → x *? y.

Lemma ltpinfty_adde_def : {in [pred x | x < +oo] &, ∀ x y, x +? y}.

Lemma ltninfty_adde_def : {in [pred x | -oo < x] &, ∀ x y, x +? y}.

Lemma abse_eq0 x : (`|x| == 0) = (x == 0).

Lemma abse0 : `|0| = 0 :> \bar R.

Lemma abse1 : `|1| = 1 :> \bar R.

Lemma abseN x : `|- x| = `|x|.

Lemma eqe_opp x y : (- x == - y) = (x == y).

Lemma eqe_oppP x y : (- x = - y) ↔ (x = y).

Lemma eqe_oppLR x y : (- x == y) = (x == - y).

Lemma eqe_oppLRP x y : (- x = y) ↔ (x = - y).

Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).

Lemma oppeB x y : x +? - y → - (x - y) = - x + y.

Lemma fin_num_oppeB x y : y \is a fin_num → - (x - y) = - x + y.

Lemma fin_numD x y :
  (x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).

Lemma sum_fin_num (T : Type) (s : seq T) (P : pred T) (f : T → \bar R) :
  \sum_(i <- s | P i) f i \is a fin_num =
  all [pred x | x \is a fin_num] [seq f i | i <- s & P i].

Lemma sum_fin_numP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
  reflect (∀ i, i \in s → P i → f i \is a fin_num)
          (\sum_(i <- s | P i) f i \is a fin_num).

Lemma fin_numB x y :
  (x - y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).

Lemma fin_numM x y : x \is a fin_num → y \is a fin_num →
  x × y \is a fin_num.

Lemma fin_numX x n : x \is a fin_num → x ^+ n \is a fin_num.

Lemma fineD : {in @fin_num R &, {morph fine : x y / x + y >-> (x + y)%R}}.

Lemma fineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.

Lemma fineM : {in @fin_num R &, {morph fine : x y / x × y >-> (x × y)%R}}.

Lemma fineK x : x \is a fin_num → (fine x)%:E = x.

Lemma EFin_sum_fine (I : Type) s (P : pred I) (f : I → \bar R) :
    (∀ i, P i → f i \is a fin_num) →
  (\sum_(i <- s | P i) fine (f i))%:E = \sum_(i <- s | P i) f i.

Lemma sum_fine (I : Type) s (P : pred I) (F : I → \bar R) :
    (∀ i, P i → F i \is a fin_num) →
  (\sum_(i <- s | P i) fine (F i) = fine (\sum_(i <- s | P i) F i))%R.

Lemma sumeN I s (P : pred I) (f : I → \bar R) :
    {in P &, ∀ i j, f i +? f j} →
  \sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.

Lemma fin_num_sumeN I s (P : pred I) (f : I → \bar R) :
    (∀ i, P i → f i \is a fin_num) →
  \sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.

Lemma telescope_sume n m (f : nat → \bar R) :
  (∀ i, (n ≤ i ≤ m)%N → f i \is a fin_num) → (n ≤ m)%N →
  \sum_(n ≤ k < m) (f k.+1 - f k) = f m - f n.

Lemma addeK x y : x \is a fin_num → y + x - x = y.

Lemma subeK x y : y \is a fin_num → x - y + y = x.

Lemma subee x : x \is a fin_num → x - x = 0.

Lemma sube_eq x y z : x \is a fin_num → (y +? z) →
  (x - z == y) = (x == y + z).

Lemma adde_eq_ninfty x y : (x + y == -oo) = ((x == -oo) || (y == -oo)).

Lemma addye x : x != -oo → +oo + x = +oo.

Lemma addey x : x != -oo → x + +oo = +oo.

Lemma addNye x : -oo + x = -oo.

Lemma addeNy x : x + -oo = -oo.

Lemma adde_Neq_pinfty x y : x != -oo → y != -oo →
  (x + y != +oo) = (x != +oo) && (y != +oo).

Lemma adde_Neq_ninfty x y : x != +oo → y != +oo →
  (x + y != -oo) = (x != -oo) && (y != -oo).

Lemma adde_ss_eq0 x y : (0 ≤ x) && (0 ≤ y) || (x ≤ 0) && (y ≤ 0) →
  x + y == 0 = (x == 0) && (y == 0).

Lemma esum_eqNyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
  \sum_(i <- s | P i) f i = -oo ↔ ∃ i, [/\ i \in s, P i & f i = -oo].

Lemma esum_eqNy (I : finType) (f : I → \bar R) (P : {pred I}) :
  (\sum_(i | P i) f i == -oo) = [∃ i in P, f i == -oo].

Lemma esum_eqyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
  (∀ i, P i → f i != -oo) →
  \sum_(i <- s | P i) f i = +oo ↔ ∃ i, [/\ i \in s, P i & f i = +oo].

Lemma esum_eqy (I : finType) (P : {pred I}) (f : I → \bar R) :
  (∀ i, P i → f i != -oo) →
  (\sum_(i | P i) f i == +oo) = [∃ i in P, f i == +oo].

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNyP`")]
Notation esum_ninftyP := esum_eqNyP (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNy`")]
Notation esum_ninfty := esum_eqNy (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqyP`")]
Notation esum_pinftyP := esum_eqyP (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqy`")]
Notation esum_pinfty := esum_eqy (only parsing).

Lemma adde_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.

Lemma adde_le0 x y : x ≤ 0 → y ≤ 0 → x + y ≤ 0.

Lemma oppe_gt0 x : (0 < - x) = (x < 0).

Lemma oppe_lt0 x : (- x < 0) = (0 < x).

Lemma oppe_ge0 x : (0 ≤ - x) = (x ≤ 0).

Lemma oppe_le0 x : (- x ≤ 0) = (0 ≤ x).

Lemma sume_ge0 T (f : T → \bar R) (P : pred T) :
  (∀ t, P t → 0 ≤ f t) → ∀ l, 0 ≤ \sum_(i <- l | P i) f i.

Lemma sume_le0 T (f : T → \bar R) (P : pred T) :
  (∀ t, P t → f t ≤ 0) → ∀ l, \sum_(i <- l | P i) f i ≤ 0.

Lemma mulNyy : -oo × +oo = -oo :> \bar R.

Lemma mulyNy : +oo × -oo = -oo :> \bar R.

Lemma mulyy : +oo × +oo = +oo :> \bar R.

Lemma mulNyNy : -oo × -oo = +oo :> \bar R.

Lemma real_mulry r : r \is Num.real → r%:E × +oo = (Num.sg r)%:E × +oo.

Lemma real_mulyr r : r \is Num.real → +oo × r%:E = (Num.sg r)%:E × +oo.

Lemma real_mulrNy r : r \is Num.real → r%:E × -oo = (Num.sg r)%:E × -oo.

Lemma real_mulNyr r : r \is Num.real → -oo × r%:E = (Num.sg r)%:E × -oo.

Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).

Lemma mulN1e x : - 1%E × x = - x.

Lemma muleN1 x : x × - 1%E = - x.

Lemma mule_neq0 x y : x != 0 → y != 0 → x × y != 0.

Lemma mule_eq0 x y : (x × y == 0) = (x == 0) || (y == 0).

Lemma mule_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.

Lemma mule_gt0 x y : 0 < x → 0 < y → 0 < x × y.

Lemma mule_le0 x y : x ≤ 0 → y ≤ 0 → 0 ≤ x × y.

Lemma mule_le0_ge0 x y : x ≤ 0 → 0 ≤ y → x × y ≤ 0.

Lemma mule_ge0_le0 x y : 0 ≤ x → y ≤ 0 → x × y ≤ 0.

Lemma mule_lt0_lt0 x y : x < 0 → y < 0 → 0 < x × y.

Lemma mule_gt0_lt0 x y : 0 < x → y < 0 → x × y < 0.

Lemma mule_lt0_gt0 x y : x < 0 → 0 < y → x × y < 0.

Lemma gte_opp x : 0 < x → - x < x.

Lemma realMe x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x × y)%O.

Lemma sqreD x y : x + y \is a fin_num →
  (x + y) ^+ 2 = x ^+ 2 + x × y *+ 2 + y ^+ 2.

Lemma abse_ge0 x : 0 ≤ `|x|.

Lemma gee0_abs x : 0 ≤ x → `|x| = x.

Lemma gte0_abs x : 0 < x → `|x| = x.

Lemma lee0_abs x : x ≤ 0 → `|x| = - x.

Lemma lte0_abs x : x < 0 → `|x| = - x.

End ERealArithTh_numDomainType.
Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope.
Notation "x +? y" := (adde_def x y) : ereal_scope.
Notation "x *? y" := (mule_def x%dE y%dE) : ereal_dual_scope.
Notation "x *? y" := (mule_def x y) : ereal_scope.

Notation maxe := (@Order.max ereal_display _).
Notation "@ 'maxe' R" := (@Order.max ereal_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.

Notation mine := (@Order.min ereal_display _).
Notation "@ 'mine' R" := (@Order.min ereal_display R)
  (at level 10, R at level 8, only parsing) : fun_scope.

Module DualAddTheoryNumDomain.

Section DualERealArithTh_numDomainType.

Local Open Scope ereal_dual_scope.

Context {R : numDomainType}.

Implicit Types x y z : \bar R.

Lemma dual_addeE x y : (x + y)%dE = - ((- x) + (- y))%E.

Lemma dual_sumeE I (r : seq I) (P : pred I) (F : I → \bar R) :
  (\sum_(i <- r | P i) F i)%dE = - (\sum_(i <- r | P i) (- F i)%E)%E.

Lemma dual_addeE_def x y : x +? y → (x + y)%dE = (x + y)%E.

Lemma dEFinD (r r' : R) : (r + r')%R%:E = r%:E + r'%:E.

Lemma dEFinB (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.

Lemma dsumEFin I r P (F : I → R) :
  \sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E.

Lemma daddeC : commutative (S := \bar R) +%dE.

Lemma dadde0 : right_id (0 : \bar R) +%dE.

Lemma dadd0e : left_id (0 : \bar R) +%dE.

Lemma daddeA : associative (S := \bar R) +%dE.

Canonical dadde_monoid := Monoid.Law daddeA dadd0e dadde0.
Canonical dadde_comoid := Monoid.ComLaw daddeC.

Lemma daddeAC : right_commutative (S := \bar R) +%dE.

Lemma daddeCA : left_commutative (S := \bar R) +%dE.

Lemma daddeACA : @interchange (\bar R) +%dE +%dE.

Lemma realDed x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x + y)%O.

Lemma doppeD x y : x +? y → - (x + y) = - x - y.

Lemma fin_num_doppeD x y : y \is a fin_num → - (x + y) = - x - y.

Lemma dsube0 x : x - 0 = x.

Lemma dsub0e x : 0 - x = - x.

Lemma doppeB x y : x +? - y → - (x - y) = - x + y.

Lemma fin_num_doppeB x y : y \is a fin_num → - (x - y) = - x + y.

Lemma dfin_numD x y :
  (x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).

Lemma dfineD :
  {in (@fin_num R) &, {morph fine : x y / x + y >-> (x + y)%R}}.

Lemma dfineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.

Lemma daddeK x y : x \is a fin_num → y + x - x = y.

Lemma dsubeK x y : y \is a fin_num → x - y + y = x.

Lemma dsubee x : x \is a fin_num → x - x = 0.

Lemma dsube_eq x y z : x \is a fin_num → (y +? z) →
  (x - z == y) = (x == y + z).

Lemma dadde_eq_pinfty x y : (x + y == +oo) = ((x == +oo) || (y == +oo)).

Lemma daddye x : +oo + x = +oo.

Lemma daddey x : x + +oo = +oo.

Lemma daddNye x : x != +oo → -oo + x = -oo.

Lemma daddeNy x : x != +oo → x + -oo = -oo.

#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed `daddye` and generalized")]
Lemma daddooe x : x != -oo → +oo + x = +oo.

#[deprecated(since="mathcomp-analysis 0.6.0",
  note="renamed `daddey` and generalized")]
Lemma daddeoo x : x != -oo → x + +oo = +oo.

Lemma dadde_Neq_pinfty x y : x != -oo → y != -oo →
  (x + y != +oo) = (x != +oo) && (y != +oo).

Lemma dadde_Neq_ninfty x y : x != +oo → y != +oo →
  (x + y != -oo) = (x != -oo) && (y != -oo).

Lemma ndadde_eq0 x y : x ≤ 0 → y ≤ 0 → x + y == 0 = (x == 0) && (y == 0).

Lemma pdadde_eq0 x y : 0 ≤ x → 0 ≤ y → x + y == 0 = (x == 0) && (y == 0).

Lemma dadde_ss_eq0 x y : (0 ≤ x) && (0 ≤ y) || (x ≤ 0) && (y ≤ 0) →
  x + y == 0 = (x == 0) && (y == 0).

Lemma desum_eqyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
  \sum_(i <- s | P i) f i = +oo ↔ ∃ i, [/\ i \in s, P i & f i = +oo].

Lemma desum_eqy (I : finType) (f : I → \bar R) (P : {pred I}) :
  (\sum_(i | P i) f i == +oo) = [∃ i in P, f i == +oo].

Lemma desum_eqNyP
    (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
  (∀ i, P i → f i != +oo) →
  \sum_(i <- s | P i) f i = -oo ↔ ∃ i, [/\ i \in s, P i & f i = -oo].

Lemma desum_eqNy (I : finType) (f : I → \bar R) (P : {pred I}) :
  (∀ i, f i != +oo) →
  (\sum_(i | P i) f i == -oo) = [∃ i in P, f i == -oo].

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNyP`")]
Notation desum_ninftyP := desum_eqNyP (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqNy`")]
Notation desum_ninfty := desum_eqNy (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqyP`")]
Notation desum_pinftyP := desum_eqyP (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `desum_eqy`")]
Notation desum_pinfty := desum_eqy (only parsing).

Lemma dadde_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.

Lemma dadde_le0 x y : x ≤ 0 → y ≤ 0 → x + y ≤ 0.

Lemma dsume_ge0 T (f : T → \bar R) (P : pred T) :
  (∀ n, P n → 0 ≤ f n) → ∀ l, 0 ≤ \sum_(i <- l | P i) f i.

Lemma dsume_le0 T (f : T → \bar R) (P : pred T) :
  (∀ n, P n → f n ≤ 0) → ∀ l, \sum_(i <- l | P i) f i ≤ 0.

Lemma gte_dopp (r : \bar R) : (0 < r)%E → (- r < r)%E.

Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.

Lemma ednatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.

Lemma EFin_dnatmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.

Lemma ednatmulE x n : x *+ n = (x *+ n)%E.

Lemma dmule2n x : x *+ 2 = x + x.

Lemma sqredD x y : x + y \is a fin_num →
  (x + y) ^+ 2 = x ^+ 2 + x × y *+ 2 + y ^+ 2.

End DualERealArithTh_numDomainType.

End DualAddTheoryNumDomain.

Section ERealArithTh_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y z u a b : \bar R) (r : R).

Lemma fin_numElt x : (x \is a fin_num) = (-oo < x < +oo).

Lemma fin_numPlt x : reflect (-oo < x < +oo) (x \is a fin_num).

Lemma ltey_eq x : (x < +oo) = (x \is a fin_num) || (x == -oo).

Lemma ltNye_eq x : (-oo < x) = (x \is a fin_num) || (x == +oo).

Lemma ge0_fin_numE x : 0 ≤ x → (x \is a fin_num) = (x < +oo).

Lemma gt0_fin_numE x : 0 < x → (x \is a fin_num) = (x < +oo).

Lemma le0_fin_numE x : x ≤ 0 → (x \is a fin_num) = (-oo < x).

Lemma lt0_fin_numE x : x < 0 → (x \is a fin_num) = (-oo < x).

Lemma eqyP x : x = +oo ↔ (∀ A, (0 < A)%R → A%:E ≤ x).

#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `eqyP`")]
Notation eq_pinftyP := eqyP (only parsing).

Lemma seq_psume_eq0 (I : choiceType) (r : seq I)
    (P : pred I) (F : I → \bar R) : (∀ i, P i → 0 ≤ F i)%E →
  (\sum_(i <- r | P i) F i == 0)%E = all (fun i ⇒ P i ==> (F i == 0%E)) r.

Lemma lte_add_pinfty x y : x < +oo → y < +oo → x + y < +oo.

Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I → \bar R) :
  (∀ i, P i → f i < +oo) → \sum_(i <- s | P i) f i < +oo.

Lemma sube_gt0 x y : (0 < y - x) = (x < y).

Lemma sube_le0 x y : (y - x ≤ 0) = (y ≤ x).

Lemma suber_ge0 y x : y \is a fin_num → (0 ≤ x - y) = (y ≤ x).

Lemma subre_ge0 x y : y \is a fin_num → (0 ≤ y - x) = (x ≤ y).

Lemma sube_ge0 x y : (x \is a fin_num) || (y \is a fin_num) →
  (0 ≤ y - x) = (x ≤ y).

Lemma lte_oppl x y : (- x < y) = (- y < x).

Lemma lte_oppr x y : (x < - y) = (y < - x).

Lemma lee_oppr x y : (x ≤ - y) = (y ≤ - x).

Lemma lee_oppl x y : (- x ≤ y) = (- y ≤ x).

Lemma muleN x y : x × - y = - (x × y).

Lemma mulNe x y : - x × y = - (x × y).

Lemma muleNN x y : - x × - y = x × y.

Lemma mulry r : r%:E × +oo%E = (Num.sg r)%:E × +oo%E.

Lemma mulyr r : +oo%E × r%:E = (Num.sg r)%:E × +oo%E.

Lemma mulrNy r : r%:E × -oo%E = (Num.sg r)%:E × -oo%E.

Lemma mulNyr r : -oo%E × r%:E = (Num.sg r)%:E × -oo%E.

Definition mulr_infty := (mulry, mulyr, mulrNy, mulNyr).

Lemma lte_mul_pinfty x y : 0 ≤ x → x \is a fin_num → y < +oo → x × y < +oo.

Lemma mule_ge0_gt0 x y : 0 ≤ x → 0 ≤ y → (0 < x × y) = (0 < x) && (0 < y).

Lemma gt0_mulye x : (0 < x → +oo × x = +oo)%E.

Lemma lt0_mulye x : (x < 0 → +oo × x = -oo)%E.

Lemma gt0_mulNye x : (0 < x → -oo × x = -oo)%E.

Lemma lt0_mulNye x : (x < 0 → -oo × x = +oo)%E.

Lemma gt0_muley x : (0 < x → x × +oo = +oo)%E.

Lemma lt0_muley x : (x < 0 → x × +oo = -oo)%E.

Lemma gt0_muleNy x : (0 < x → x × -oo = -oo)%E.

Lemma lt0_muleNy x : (x < 0 → x × -oo = +oo)%E.

Lemma mule_eq_pinfty x y : (x × y == +oo) =
  [|| (x > 0) && (y == +oo), (x < 0) && (y == -oo),
     (x == +oo) && (y > 0) | (x == -oo) && (y < 0)].

Lemma mule_eq_ninfty x y : (x × y == -oo) =
  [|| (x > 0) && (y == -oo), (x < 0) && (y == +oo),
     (x == -oo) && (y > 0) | (x == +oo) && (y < 0)].

Lemma lteN2 x y : (- x < - y) = (y < x).

Lemma lte_add a b x y : a < b → x < y → a + x < b + y.

Lemma lee_addl x y : 0 ≤ y → x ≤ x + y.

Lemma lee_addr x y : 0 ≤ y → x ≤ y + x.

Lemma gee_addl x y : y ≤ 0 → x + y ≤ x.

Lemma gee_addr x y : y ≤ 0 → y + x ≤ x.

Lemma lte_addl y x : y \is a fin_num → (y < y + x) = (0 < x).

Lemma lte_addr y x : y \is a fin_num → (y < x + y) = (0 < x).

Lemma gte_subl y x : y \is a fin_num → (y - x < y) = (0 < x).

Lemma gte_subr y x : y \is a fin_num → (- x + y < y) = (0 < x).

Lemma gte_addl x y : x \is a fin_num → (x + y < x) = (y < 0).

Lemma gte_addr x y : x \is a fin_num → (y + x < x) = (y < 0).

Lemma lte_add2lE x a b : x \is a fin_num → (x + a < x + b) = (a < b).

Lemma lee_add2l x a b : a ≤ b → x + a ≤ x + b.

Lemma lee_add2lE x a b : x \is a fin_num → (x + a ≤ x + b) = (a ≤ b).

Lemma lee_add2r x a b : a ≤ b → a + x ≤ b + x.

Lemma lee_add a b x y : a ≤ b → x ≤ y → a + x ≤ b + y.

Lemma lte_le_add a b x y : b \is a fin_num → a < x → b ≤ y → a + b < x + y.

Lemma lee_lt_add a b x y : a \is a fin_num → a ≤ x → b < y → a + b < x + y.

Lemma lee_sub x y z u : x ≤ y → u ≤ z → x - z ≤ y - u.

Lemma lte_le_sub z u x y : u \is a fin_num →
  x < z → u ≤ y → x - y < z - u.

Lemma lte_pmul2r z : z \is a fin_num → 0 < z → {mono *%E^~ z : x y / x < y}.

Lemma lte_pmul2l z : z \is a fin_num → 0 < z → {mono *%E z : x y / x < y}.

Lemma lte_nmul2l z : z \is a fin_num → z < 0 → {mono *%E z : x y /~ x < y}.

Lemma lte_nmul2r z : z \is a fin_num → z < 0 → {mono *%E^~ z : x y /~ x < y}.

Lemma lte_pmulr x y : y \is a fin_num → 0 < y → (y < y × x) = (1 < x).

Lemma lte_pmull x y : y \is a fin_num → 0 < y → (y < x × y) = (1 < x).

Lemma lte_nmulr x y : y \is a fin_num → y < 0 → (y < y × x) = (x < 1).

Lemma lte_nmull x y : y \is a fin_num → y < 0 → (y < x × y) = (x < 1).

Lemma lee_sum I (f g : I → \bar R) s (P : pred I) :
  (∀ i, P i → f i ≤ g i) →
  \sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i) g i.

Lemma lee_sum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
  {subset Q ≤ P} → {in [predD P & Q], ∀ i, 0 ≤ f i} →
  \sum_(i <- s | Q i) f i ≤ \sum_(i <- s | P i) f i.

Lemma lee_sum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
  {subset Q ≤ P} → {in [predD P & Q], ∀ i, f i ≤ 0} →
  \sum_(i <- s | P i) f i ≤ \sum_(i <- s | Q i) f i.

Lemma lee_sum_nneg (I : eqType) (s : seq I) (P Q : pred I)
  (f : I → \bar R) : (∀ i, P i → ~~ Q i → 0 ≤ f i) →
  \sum_(i <- s | P i && Q i) f i ≤ \sum_(i <- s | P i) f i.

Lemma lee_sum_npos (I : eqType) (s : seq I) (P Q : pred I)
  (f : I → \bar R) : (∀ i, P i → ~~ Q i → f i ≤ 0) →
  \sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i && Q i) f i.

Lemma lee_sum_nneg_ord (f : nat → \bar R) (P : pred nat) :
  (∀ n, P n → 0 ≤ f n) →
  {homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.

Lemma lee_sum_npos_ord (f : nat → \bar R) (P : pred nat) :
  (∀ n, P n → f n ≤ 0) →
  {homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.

Lemma lee_sum_nneg_natr (f : nat → \bar R) (P : pred nat) m :
  (∀ n, (m ≤ n)%N → P n → 0 ≤ f n) →
  {homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.

Lemma lee_sum_npos_natr (f : nat → \bar R) (P : pred nat) m :
  (∀ n, (m ≤ n)%N → P n → f n ≤ 0) →
  {homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.

Lemma lee_sum_nneg_natl (f : nat → \bar R) (P : pred nat) n :
  (∀ m, (m < n)%N → P m → 0 ≤ f m) →
  {homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.

Lemma lee_sum_npos_natl (f : nat → \bar R) (P : pred nat) n :
  (∀ m, (m < n)%N → P m → f m ≤ 0) →
  {homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.

Lemma lee_sum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
  (f : T → \bar R) : {subset A ≤ B} →
  {in [predD B & A], ∀ t, P t → 0 ≤ f t} →
  \sum_(t <- A | P t) f t ≤ \sum_(t <- B | P t) f t.

Lemma lee_sum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
  (f : T → \bar R) : {subset A ≤ B} →
  {in [predD B & A], ∀ t, P t → f t ≤ 0} →
  \sum_(t <- B | P t) f t ≤ \sum_(t <- A | P t) f t.

Lemma lte_subl_addr x y z : y \is a fin_num → (x - y < z) = (x < z + y).

Lemma lte_subl_addl x y z : y \is a fin_num → (x - y < z) = (x < y + z).

Lemma lte_subr_addr x y z : z \is a fin_num → (x < y - z) = (x + z < y).

Lemma lte_subr_addl x y z : z \is a fin_num → (x < y - z) = (z + x < y).

Lemma lte_subel_addr x y z : x \is a fin_num → (x - y < z) = (x < z + y).

Lemma lte_subel_addl x y z : x \is a fin_num → (x - y < z) = (x < y + z).

Lemma lte_suber_addr x y z : x \is a fin_num → (x < y - z) = (x + z < y).

Lemma lte_suber_addl x y z : x \is a fin_num → (x < y - z) = (z + x < y).

Lemma lee_subl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + y).

Lemma lee_subl_addl x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ y + z).

Lemma lee_subr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).

Lemma lee_subr_addl x y z : z \is a fin_num → (x ≤ y - z) = (z + x ≤ y).

Lemma lee_subel_addr x y z : z \is a fin_num → (x - y ≤ z) = (x ≤ z + y).

Lemma lee_subel_addl x y z : z \is a fin_num → (x - y ≤ z) = (x ≤ y + z).

Lemma lee_suber_addr x y z : y \is a fin_num → (x ≤ y - z) = (x + z ≤ y).

Lemma lee_suber_addl x y z : y \is a fin_num → (x ≤ y - z) = (z + x ≤ y).

Lemma subre_lt0 x y : x \is a fin_num → (x - y < 0) = (x < y).

Lemma suber_lt0 x y : y \is a fin_num → (x - y < 0) = (x < y).

Lemma sube_lt0 x y : (x \is a fin_num) || (y \is a fin_num) →
  (x - y < 0) = (x < y).

Lemma pmule_rge0 x y : 0 < x → (x × y ≥ 0) = (y ≥ 0).

Lemma pmule_lge0 x y : 0 < x → (y × x ≥ 0) = (y ≥ 0).

Lemma pmule_rlt0 x y : 0 < x → (x × y < 0) = (y < 0).

Lemma pmule_llt0 x y : 0 < x → (y × x < 0) = (y < 0).

Lemma pmule_rle0 x y : 0 < x → (x × y ≤ 0) = (y ≤ 0).

Lemma pmule_lle0 x y : 0 < x → (y × x ≤ 0) = (y ≤ 0).

Lemma pmule_rgt0 x y : 0 < x → (x × y > 0) = (y > 0).

Lemma pmule_lgt0 x y : 0 < x → (y × x > 0) = (y > 0).

Lemma nmule_rge0 x y : x < 0 → (x × y ≥ 0) = (y ≤ 0).

Lemma nmule_lge0 x y : x < 0 → (y × x ≥ 0) = (y ≤ 0).

Lemma nmule_rle0 x y : x < 0 → (x × y ≤ 0) = (y ≥ 0).

Lemma nmule_lle0 x y : x < 0 → (y × x ≤ 0) = (y ≥ 0).

Lemma nmule_rgt0 x y : x < 0 → (x × y > 0) = (y < 0).

Lemma nmule_lgt0 x y : x < 0 → (y × x > 0) = (y < 0).

Lemma nmule_rlt0 x y : x < 0 → (x × y < 0) = (y > 0).

Lemma nmule_llt0 x y : x < 0 → (y × x < 0) = (y > 0).

Lemma mule_lt0 x y : (x × y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].

Lemma muleA : associative ( *%E : \bar R → \bar R → \bar R ).

Local Open Scope ereal_scope.

Canonical mule_monoid := Monoid.Law muleA mul1e mule1.
Canonical mule_comoid := Monoid.ComLaw muleC.

Lemma muleCA : left_commutative ( *%E : \bar R → \bar R → \bar R ).

Lemma muleAC : right_commutative ( *%E : \bar R → \bar R → \bar R ).

Lemma muleACA : interchange (@mule R) (@mule R).

Lemma muleDr x y z : x \is a fin_num → y +? z → x × (y + z) = x × y + x × z.

Lemma muleDl x y z : x \is a fin_num → y +? z → (y + z) × x = y × x + z × x.

Lemma muleBr x y z : x \is a fin_num → y +? - z → x × (y - z) = x × y - x × z.

Lemma muleBl x y z : x \is a fin_num → y +? - z → (y - z) × x = y × x - z × x.

Lemma ge0_muleDl x y z : 0 ≤ y → 0 ≤ z → (y + z) × x = y × x + z × x.

Lemma ge0_muleDr x y z : 0 ≤ y → 0 ≤ z → x × (y + z) = x × y + x × z.

Lemma le0_muleDl x y z : y ≤ 0 → z ≤ 0 → (y + z) × x = y × x + z × x.

Lemma le0_muleDr x y z : y ≤ 0 → z ≤ 0 → x × (y + z) = x × y + x × z.

Lemma gee_pmull y x : y \is a fin_num → 0 < x → y ≤ 1 → y × x ≤ x.

Lemma lee_wpmul2r x : 0 ≤ x → {homo *%E^~ x : y z / y ≤ z}.

Lemma lee_wpmul2l x : 0 ≤ x → {homo *%E x : y z / y ≤ z}.

Lemma ge0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → 0 ≤ F i) →
  (\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).

Lemma ge0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → 0 ≤ F i) →
  x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).

Lemma le0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → F i ≤ 0) →
  (\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).

Lemma le0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → F i ≤ 0) →
  x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).

Lemma fin_num_sume_distrr (I : Type) (s : seq I) x (P : pred I)
    (F : I → \bar R) :
  x \is a fin_num → {in P &, ∀ i j, F i +? F j} →
    x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) x × F i.

Lemma eq_infty x : (∀ r, r%:E ≤ x) → x = +oo.

Lemma eq_ninfty x : (∀ r, x ≤ r%:E) → x = -oo.

Lemma leeN2 x y : (- x ≤ - y) = (y ≤ x).

Lemma lee_abs x : x ≤ `|x|.

Lemma abse_id x : `| `|x| | = `|x|.

Lemma lte_absl (x y : \bar R) : (`|x| < y)%E = (- y < x < y)%E.

Lemma eqe_absl x y : (`|x| == y) = ((x == y) || (x == - y)) && (0 ≤ y).

Lemma lee_abs_add x y : `|x + y| ≤ `|x| + `|y|.

Lemma lee_abs_sum (I : Type) (s : seq I) (F : I → \bar R) (P : pred I) :
  `|\sum_(i <- s | P i) F i| ≤ \sum_(i <- s | P i) `|F i|.

Lemma lee_abs_sub x y : `|x - y| ≤ `|x| + `|y|.

Lemma abseM : {morph @abse R : x y / x × y}.

Lemma fine_max :
  {in fin_num &, {mono @fine R : x y / maxe x y >-> (Num.max x y)%:E}}.

Lemma EFin_max : {morph (@EFin R) : r s / Num.max r s >-> maxe r s}.

Lemma fine_min :
  {in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}.

Lemma EFin_min : {morph (@EFin R) : r s / Num.min r s >-> mine r s}.

Lemma adde_maxl : left_distributive (@adde R) maxe.

Lemma adde_maxr : right_distributive (@adde R) maxe.

Lemma maxye : left_zero (+oo : \bar R) maxe.

Lemma maxey : right_zero (+oo : \bar R) maxe.

Lemma maxNye : left_id (-oo : \bar R) maxe.

Lemma maxeNy : right_id (-oo : \bar R) maxe.

Canonical maxe_monoid := Monoid.Law maxA maxNye maxeNy.
Canonical maxe_comoid := Monoid.ComLaw maxC.

Lemma minNye : left_zero (-oo : \bar R) mine.

Lemma mineNy : right_zero (-oo : \bar R) mine.

Lemma minye : left_id (+oo : \bar R) mine.

Lemma miney : right_id (+oo : \bar R) mine.

Canonical mine_monoid := Monoid.Law minA minye miney.
Canonical mine_comoid := Monoid.ComLaw minC.

Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.

Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.

Lemma maxeMr z x y : z \is a fin_num → 0 < z →
  z × maxe x y = maxe (z × x) (z × y).

Lemma maxeMl z x y : z \is a fin_num → 0 < z →
  maxe x y × z = maxe (x × z) (y × z).

Lemma mineMr z x y : z \is a fin_num → 0 < z →
  z × mine x y = mine (z × x) (z × y).

Lemma mineMl z x y : z \is a fin_num → 0 < z →
  mine x y × z = mine (x × z) (y × z).

Lemma bigmaxe_fin_num (s : seq R) r : r \in s →
  \big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num.

Lemma lee_pemull x y : 0 ≤ y → 1 ≤ x → y ≤ x × y.

Lemma lee_nemull x y : y ≤ 0 → 1 ≤ x → x × y ≤ y.

Lemma lee_pemulr x y : 0 ≤ y → 1 ≤ x → y ≤ y × x.

Lemma lee_nemulr x y : y ≤ 0 → 1 ≤ x → y × x ≤ y.

Lemma mule_natl x n : n%:R%:E × x = x *+ n.

Lemma lte_pmul x1 y1 x2 y2 :
  0 ≤ x1 → 0 ≤ x2 → x1 < y1 → x2 < y2 → x1 × x2 < y1 × y2.

Lemma lee_pmul x1 y1 x2 y2 : 0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 → x2 ≤ y2 →
  x1 × x2 ≤ y1 × y2.

Lemma lee_pmul2l x : x \is a fin_num → 0 < x → {mono *%E x : x y / x ≤ y}.

Lemma lee_pmul2r x : x \is a fin_num → 0 < x → {mono *%E^~ x : x y / x ≤ y}.

Lemma lee_sqr x y : 0 ≤ x → 0 ≤ y → (x ^+ 2 ≤ y ^+ 2) = (x ≤ y).

Lemma lte_sqr x y : 0 ≤ x → 0 ≤ y → (x ^+ 2 < y ^+ 2) = (x < y).

Lemma lee_sqrE x y : 0 ≤ y → x ^+ 2 ≤ y ^+ 2 → x ≤ y.

Lemma lte_sqrE x y : 0 ≤ y → x ^+ 2 < y ^+ 2 → x < y.

Lemma sqre_ge0 x : 0 ≤ x ^+ 2.

Lemma lee_paddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.

Lemma lte_paddl y x z : 0 ≤ x → y < z → y < x + z.

Lemma lee_paddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.

Lemma lte_paddr y x z : 0 ≤ x → y < z → y < z + x.

Lemma lte_spaddre z x y : z \is a fin_num → 0 < y → z ≤ x → z < x + y.

Lemma lte_spadder z x y : x \is a fin_num → 0 < y → z ≤ x → z < x + y.

End ERealArithTh_realDomainType.
Arguments lee_sum_nneg_ord {R}.
Arguments lee_sum_npos_ord {R}.
Arguments lee_sum_nneg_natr {R}.
Arguments lee_sum_npos_natr {R}.
Arguments lee_sum_nneg_natl {R}.
Arguments lee_sum_npos_natl {R}.
#[global] Hint Extern 0 (is_true (0 ≤ `| _ |)%E) ⇒ solve [apply: abse_ge0] : core.

#[deprecated(since="mathcomp-analysis 0.6", note="Use lte_spaddre instead.")]
Notation lte_spaddr := lte_spaddre (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.5", note="Use leeN2 instead.")]
Notation lee_opp := leeN2 (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.5", note="Use lteN2 instead.")]
Notation lte_opp := lteN2 (only parsing).

Module DualAddTheoryRealDomain.

Section DualERealArithTh_realDomainType.

Import DualAddTheoryNumDomain.

Local Open Scope ereal_dual_scope.

Context {R : realDomainType}.
Implicit Types x y z a b : \bar R.

Lemma dsube_lt0 x y : (x - y < 0) = (x < y).

Lemma dsube_ge0 x y : (0 ≤ y - x) = (x ≤ y).

Lemma dsuber_le0 x y : y \is a fin_num → (x - y ≤ 0) = (x ≤ y).

Lemma dsubre_le0 y x : y \is a fin_num → (y - x ≤ 0) = (y ≤ x).

Lemma dsube_le0 x y : (x \is a fin_num) || (y \is a fin_num) →
  (y - x ≤ 0) = (y ≤ x).

Lemma lte_dadd a b x y : a < b → x < y → a + x < b + y.

Lemma lee_daddl x y : 0 ≤ y → x ≤ x + y.

Lemma lee_daddr x y : 0 ≤ y → x ≤ y + x.

Lemma gee_daddl x y : y ≤ 0 → x + y ≤ x.

Lemma gee_daddr x y : y ≤ 0 → y + x ≤ x.

Lemma lte_daddl y x : y \is a fin_num → (y < y + x) = (0 < x).

Lemma lte_daddr y x : y \is a fin_num → (y < x + y) = (0 < x).

Lemma gte_dsubl y x : y \is a fin_num → (y - x < y) = (0 < x).

Lemma gte_dsubr y x : y \is a fin_num → (- x + y < y) = (0 < x).

Lemma gte_daddl x y : x \is a fin_num → (x + y < x) = (y < 0).

Lemma gte_daddr x y : x \is a fin_num → (y + x < x) = (y < 0).

Lemma lte_dadd2lE x a b : x \is a fin_num → (x + a < x + b) = (a < b).

Lemma lee_dadd2l x a b : a ≤ b → x + a ≤ x + b.

Lemma lee_dadd2lE x a b : x \is a fin_num → (x + a ≤ x + b) = (a ≤ b).

Lemma lee_dadd2r x a b : a ≤ b → a + x ≤ b + x.

Lemma lee_dadd a b x y : a ≤ b → x ≤ y → a + x ≤ b + y.

Lemma lte_le_dadd a b x y : b \is a fin_num → a < x → b ≤ y → a + b < x + y.

Lemma lee_lt_dadd a b x y : a \is a fin_num → a ≤ x → b < y → a + b < x + y.

Lemma lee_dsub x y z t : x ≤ y → t ≤ z → x - z ≤ y - t.

Lemma lte_le_dsub z u x y : u \is a fin_num → x < z → u ≤ y → x - y < z - u.

Lemma lee_dsum I (f g : I → \bar R) s (P : pred I) :
  (∀ i, P i → f i ≤ g i) →
  \sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i) g i.

Lemma lee_dsum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
  {subset Q ≤ P} → {in [predD P & Q], ∀ i, 0 ≤ f i} →
  \sum_(i <- s | Q i) f i ≤ \sum_(i <- s | P i) f i.

Lemma lee_dsum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
  {subset Q ≤ P} → {in [predD P & Q], ∀ i, f i ≤ 0} →
  \sum_(i <- s | P i) f i ≤ \sum_(i <- s | Q i) f i.

Lemma lee_dsum_nneg (I : eqType) (s : seq I) (P Q : pred I)
  (f : I → \bar R) : (∀ i, P i → ~~ Q i → 0 ≤ f i) →
  \sum_(i <- s | P i && Q i) f i ≤ \sum_(i <- s | P i) f i.

Lemma lee_dsum_npos (I : eqType) (s : seq I) (P Q : pred I)
  (f : I → \bar R) : (∀ i, P i → ~~ Q i → f i ≤ 0) →
  \sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i && Q i) f i.

Lemma lee_dsum_nneg_ord (f : nat → \bar R) (P : pred nat) :
  (∀ n, P n → 0 ≤ f n)%E →
  {homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.

Lemma lee_dsum_npos_ord (f : nat → \bar R) (P : pred nat) :
  (∀ n, P n → f n ≤ 0)%E →
  {homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.

Lemma lee_dsum_nneg_natr (f : nat → \bar R) (P : pred nat) m :
  (∀ n, (m ≤ n)%N → P n → 0 ≤ f n) →
  {homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.

Lemma lee_dsum_npos_natr (f : nat → \bar R) (P : pred nat) m :
  (∀ n, (m ≤ n)%N → P n → f n ≤ 0) →
  {homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.

Lemma lee_dsum_nneg_natl (f : nat → \bar R) (P : pred nat) n :
  (∀ m, (m < n)%N → P m → 0 ≤ f m) →
  {homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.

Lemma lee_dsum_npos_natl (f : nat → \bar R) (P : pred nat) n :
  (∀ m, (m < n)%N → P m → f m ≤ 0) →
  {homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.

Lemma lee_dsum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
  (f : T → \bar R) : {subset A ≤ B} →
  {in [predD B & A], ∀ t, P t → 0 ≤ f t} →
  \sum_(t <- A | P t) f t ≤ \sum_(t <- B | P t) f t.

Lemma lee_dsum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
  (f : T → \bar R) : {subset A ≤ B} →
  {in [predD B & A], ∀ t, P t → f t ≤ 0} →
  \sum_(t <- B | P t) f t ≤ \sum_(t <- A | P t) f t.

Lemma lte_dsubl_addr x y z : y \is a fin_num → (x - y < z) = (x < z + y).

Lemma lte_dsubl_addl x y z : y \is a fin_num → (x - y < z) = (x < y + z).

Lemma lte_dsubr_addr x y z : z \is a fin_num → (x < y - z) = (x + z < y).

Lemma lte_dsubr_addl x y z : z \is a fin_num → (x < y - z) = (z + x < y).

Lemma lte_dsuber_addr x y z : y \is a fin_num → (x < y - z) = (x + z < y).

Lemma lte_dsuber_addl x y z : y \is a fin_num → (x < y - z) = (z + x < y).

Lemma lte_dsubel_addr x y z : z \is a fin_num → (x - y < z) = (x < z + y).

Lemma lte_dsubel_addl x y z : z \is a fin_num → (x - y < z) = (x < y + z).

Lemma lee_dsubl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + y).

Lemma lee_dsubl_addl x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ y + z).

Lemma lee_dsubr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).

Lemma lee_dsubr_addl x y z : z \is a fin_num → (x ≤ y - z) = (z + x ≤ y).

Lemma lee_dsubel_addr x y z : x \is a fin_num → (x - y ≤ z) = (x ≤ z + y).

Lemma lee_dsubel_addl x y z : x \is a fin_num → (x - y ≤ z) = (x ≤ y + z).

Lemma lee_dsuber_addr x y z : x \is a fin_num → (x ≤ y - z) = (x + z ≤ y).

Lemma lee_dsuber_addl x y z : x \is a fin_num → (x ≤ y - z) = (z + x ≤ y).

Lemma dsuber_gt0 x y : x \is a fin_num → (0 < y - x) = (x < y).

Lemma dsubre_gt0 x y : y \is a fin_num → (0 < y - x) = (x < y).

Lemma dsube_gt0 x y : (x \is a fin_num) || (y \is a fin_num) →
  (0 < y - x) = (x < y).

Lemma dmuleDr x y z : x \is a fin_num → y +? z → x × (y + z) = x × y + x × z.

Lemma dmuleDl x y z : x \is a fin_num → y +? z → (y + z) × x = y × x + z × x.

Lemma dge0_muleDl x y z : 0 ≤ y → 0 ≤ z → (y + z) × x = y × x + z × x.

Lemma dge0_muleDr x y z : 0 ≤ y → 0 ≤ z → x × (y + z) = x × y + x × z.

Lemma dle0_muleDl x y z : y ≤ 0 → z ≤ 0 → (y + z) × x = y × x + z × x.

Lemma dle0_muleDr x y z : y ≤ 0 → z ≤ 0 → x × (y + z) = x × y + x × z.

Lemma ge0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → 0 ≤ F i) →
  (\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).

Lemma ge0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → 0 ≤ F i) →
  x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).

Lemma le0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → F i ≤ 0) →
  (\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).

Lemma le0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
  (∀ i, P i → F i ≤ 0) →
  x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).

Lemma lee_abs_dadd x y : `|x + y| ≤ `|x| + `|y|.

Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I → \bar R) (P : pred I) :
  `|\sum_(i <- s | P i) F i| ≤ \sum_(i <- s | P i) `|F i|.

Lemma lee_abs_dsub x y : `|x - y| ≤ `|x| + `|y|.

Lemma dadde_minl : left_distributive (@dual_adde R) mine.

Lemma dadde_minr : right_distributive (@dual_adde R) mine.

Lemma dmule_natl x n : n%:R%:E × x = x *+ n.

Lemma lee_pdaddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.

Lemma lte_pdaddl y x z : 0 ≤ x → y < z → y < x + z.

Lemma lee_pdaddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.

Lemma lte_pdaddr y x z : 0 ≤ x → y < z → y < z + x.

Lemma lte_spdaddre z x y : z \is a fin_num → 0 < y → z ≤ x → z < x + y.

Lemma lte_spdadder z x y : x \is a fin_num → 0 < y → z ≤ x → z < x + y.

End DualERealArithTh_realDomainType.
Arguments lee_dsum_nneg_ord {R}.
Arguments lee_dsum_npos_ord {R}.
Arguments lee_dsum_nneg_natr {R}.
Arguments lee_dsum_npos_natr {R}.
Arguments lee_dsum_nneg_natl {R}.
Arguments lee_dsum_npos_natl {R}.

End DualAddTheoryRealDomain.

Lemma lee_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x ≤ y}.

Lemma lte_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x < y}.

Section realFieldType_lemmas.
Variable R : realFieldType.
Implicit Types x y : \bar R.
Implicit Types r : R.

Lemma lee_addgt0Pr x y :
  reflect (∀ e, (0 < e)%R → x ≤ y + e%:E) (x ≤ y).

Lemma lee_mul01Pr x y : 0 ≤ x →
  reflect (∀ r, (0 < r < 1)%R → r%:E × x ≤ y) (x ≤ y).

Lemma lte_pdivr_mull r x y : (0 < r)%R → (r^-1%:E × y < x) = (y < r%:E × x).

Lemma lte_pdivr_mulr r x y : (0 < r)%R → (y × r^-1%:E < x) = (y < x × r%:E).

Lemma lte_pdivl_mull r y x : (0 < r)%R → (x < r^-1%:E × y) = (r%:E × x < y).

Lemma lte_pdivl_mulr r x y : (0 < r)%R → (x < y × r^-1%:E) = (x × r%:E < y).

Lemma lte_ndivl_mulr r x y : (r < 0)%R → (x < y × r^-1%:E) = (y < x × r%:E).

Lemma lte_ndivl_mull r x y : (r < 0)%R → (x < r^-1%:E × y) = (y < r%:E × x).

Lemma lte_ndivr_mull r x y : (r < 0)%R → (r^-1%:E × y < x) = (r%:E × x < y).

Lemma lte_ndivr_mulr r x y : (r < 0)%R → (y × r^-1%:E < x) = (x × r%:E < y).

Lemma lee_pdivr_mull r x y : (0 < r)%R → (r^-1%:E × y ≤ x) = (y ≤ r%:E × x).

Lemma lee_pdivr_mulr r x y : (0 < r)%R → (y × r^-1%:E ≤ x) = (y ≤ x × r%:E).

Lemma lee_pdivl_mull r y x : (0 < r)%R → (x ≤ r^-1%:E × y) = (r%:E × x ≤ y).

Lemma lee_pdivl_mulr r x y : (0 < r)%R → (x ≤ y × r^-1%:E) = (x × r%:E ≤ y).

Lemma lee_ndivl_mulr r x y : (r < 0)%R → (x ≤ y × r^-1%:E) = (y ≤ x × r%:E).

Lemma lee_ndivl_mull r x y : (r < 0)%R → (x ≤ r^-1%:E × y) = (y ≤ r%:E × x).

Lemma lee_ndivr_mull r x y : (r < 0)%R → (r^-1%:E × y ≤ x) = (r%:E × x ≤ y).

Lemma lee_ndivr_mulr r x y : (r < 0)%R → (y × r^-1%:E ≤ x) = (x × r%:E ≤ y).

Lemma eqe_pdivr_mull r x y : (r != 0)%R →
  ((r^-1)%:E × y == x) = (y == r%:E × x).

End realFieldType_lemmas.

Module DualAddTheoryRealField.

Import DualAddTheoryNumDomain DualAddTheoryRealDomain.

Section DualRealFieldType_lemmas.
Local Open Scope ereal_dual_scope.
Variable R : realFieldType.
Implicit Types x y : \bar R.

Lemma lee_daddgt0Pr x y :
  reflect (∀ e, (0 < e)%R → x ≤ y + e%:E) (x ≤ y).

End DualRealFieldType_lemmas.

End DualAddTheoryRealField.

Section sqrte.
Variable R : rcfType.
Implicit Types x y : \bar R.

Definition sqrte x :=
  if x is +oo then +oo else if x is r%:E then (Num.sqrt r)%:E else 0.

Lemma sqrte0 : sqrte 0 = 0 :> \bar R.

Lemma sqrte_ge0 x : 0 ≤ sqrte x.

Lemma lee_sqrt x y : 0 ≤ y → (sqrte x ≤ sqrte y) = (x ≤ y).

Lemma sqrteM x y : 0 ≤ x → sqrte (x × y) = sqrte x × sqrte y.

Lemma sqr_sqrte x : 0 ≤ x → sqrte x ^+ 2 = x.

Lemma sqrte_sqr x : sqrte (x ^+ 2) = `|x|%E.

Lemma sqrte_fin_num x : 0 ≤ x → (sqrte x \is a fin_num) = (x \is a fin_num).

End sqrte.

Module DualAddTheory.
Export DualAddTheoryNumDomain.
Export DualAddTheoryRealDomain.
Export DualAddTheoryRealField.
End DualAddTheory.

Module ConstructiveDualAddTheory.
Export DualAddTheory.
End ConstructiveDualAddTheory.

Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}.
Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}.
Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.

Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
  : ereal_dual_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
  : ereal_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
  : ereal_dual_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
  : ereal_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
    !=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
  (only printing) : ereal_dual_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
    !=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
  (only printing) : ereal_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
    ?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
  (only printing) : ereal_dual_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
    (@Signed.from _ _ _ _ _ _ (Phantom _ x))
    ?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
  (only printing) : ereal_scope.

#[global] Hint Extern 0 (is_true (0%E < _)%O) ⇒ solve [apply: gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%E)%O) ⇒ solve [apply: lt0] : core.
#[global] Hint Extern 0 (is_true (0%E ≤ _)%O) ⇒ solve [apply: ge0] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 0%E)%O) ⇒ solve [apply: le0] : core.
#[global] Hint Extern 0 (is_true (0%E >=< _)%O) ⇒ solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (_ != 0%E)%O) ⇒ solve [apply: neq0] : core.

Section SignedNumDomainStability.
Context {R : numDomainType}.

Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R).

Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).

Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R).

Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).

Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) :
  Signed.spec 0 nz cond x%:num%:E.

Canonical EFin_snum nz cond (x : {num R & nz & cond}) :=
  Signed.mk (EFin_snum_subproof x).

Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr}) :
  Signed.spec 0%R ?=0 xr (fine x%:num).

Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr}) :=
  Signed.mk (fine_snum_subproof x).

Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) :
  Signed.spec 0 xnz r (- x%:num).

Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr}) :=
  Signed.mk (oppe_snum_subproof x).

Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity)
    (xr yr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr})
    (y : {compare (0 : \bar R) & ynz & yr})
    (rnz := add_nonzero_subdef xnz ynz xr yr)
    (rrl := add_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num + y%:num).

Canonical adde_snum (xnz ynz : KnownSign.nullity)
    (xr yr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr})
    (y : {compare (0 : \bar R) & ynz & yr}) :=
  Signed.mk (adde_snum_subproof x y).

Import DualAddTheory.

Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity)
    (xr yr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr})
    (y : {compare (0 : \bar R) & ynz & yr})
    (rnz := add_nonzero_subdef xnz ynz xr yr)
    (rrl := add_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num + y%:num)%dE.

Canonical dadde_snum (xnz ynz : KnownSign.nullity)
    (xr yr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr})
    (y : {compare (0 : \bar R) & ynz & yr}) :=
  Signed.mk (dadde_snum_subproof x y).

Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity)
    (xr yr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr})
    (y : {compare (0 : \bar R) & ynz & yr})
    (rnz := mul_nonzero_subdef xnz ynz xr yr)
    (rrl := mul_reality_subdef xnz ynz xr yr) :
  Signed.spec 0 rnz rrl (x%:num × y%:num).

Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr})
    (y : {compare (0 : \bar R) & ynz & yr}) :=
  Signed.mk (mule_snum_subproof x y).

Definition abse_reality_subdef (xnz : KnownSign.nullity)
    (xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign.
Arguments abse_reality_subdef /.

Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) :
  Signed.spec 0 xnz r `|x%:num|.

Canonical abse_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
    (x : {compare (0 : \bar R) & xnz & xr}) :=
  Signed.mk (abse_snum_subproof x).

End SignedNumDomainStability.

Section MorphNum.
Context {R : numDomainType} {nz : KnownSign.nullity} {cond : KnownSign.reality}.
Implicit Types (a : \bar R).

Lemma num_abse_eq0 a : (`|a|%:nng == 0%:nng) = (a == 0).

End MorphNum.

Section MorphReal.
Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}.
Implicit Type x y : nR.

Lemma num_lee_maxr a x y :
  a ≤ maxe x%:num y%:num = (a ≤ x%:num) || (a ≤ y%:num).

Lemma num_lee_maxl a x y :
  maxe x%:num y%:num ≤ a = (x%:num ≤ a) && (y%:num ≤ a).

Lemma num_lee_minr a x y :
  a ≤ mine x%:num y%:num = (a ≤ x%:num) && (a ≤ y%:num).

Lemma num_lee_minl a x y :
  mine x%:num y%:num ≤ a = (x%:num ≤ a) || (y%:num ≤ a).

Lemma num_lte_maxr a x y :
  a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).

Lemma num_lte_maxl a x y :
  maxe x%:num y%:num < a = (x%:num < a) && (y%:num < a).

Lemma num_lte_minr a x y :
  a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).

Lemma num_lte_minl a x y :
  mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).

End MorphReal.

Section MorphGe0.
Context {R : numDomainType} {nz : KnownSign.nullity}.
Implicit Type x y : nR.

Lemma num_abse_le a x : 0 ≤ a → (`|a|%:nng ≤ x)%O = (a ≤ x%:num).

Lemma num_abse_lt a x : 0 ≤ a → (`|a|%:nng < x)%O = (a < x%:num).
End MorphGe0.

Variant posnume_spec (R : numDomainType) (x : \bar R) :
  \bar R → bool → bool → bool → Type :=
| IsPinftyPosnume :
  posnume_spec x +oo false true true
| IsRealPosnume (p : {posnum R}) :
  posnume_spec x (p%:num%:E) false true true.

Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x →
  posnume_spec x x (x == 0) (0 ≤ x) (0 < x).

Variant nonnege_spec (R : numDomainType) (x : \bar R) :
  \bar R → bool → Type :=
| IsPinftyNonnege : nonnege_spec x +oo true
| IsRealNonnege (p : {nonneg R}) : nonnege_spec x (p%:num%:E) true.

Lemma nonnegeP (R : numDomainType) (x : \bar R) : 0 ≤ x →
  nonnege_spec x x (0 ≤ x).

Section contract_expand.
Variable R : realFieldType.
Implicit Types (x : \bar R) (r : R).
Local Open Scope ereal_scope.

Definition contract x : R :=
  match x with
  | r%:E ⇒ r / (1 + `|r|) | +oo ⇒ 1 | -oo ⇒ -1
  end.

Lemma contract_lt1 r : (`|contract r%:E| < 1)%R.

Lemma contract_le1 x : (`|contract x| ≤ 1)%R.

Lemma contract0 : contract 0 = 0%R.

Lemma contractN x : contract (- x) = (- contract x)%R.