Module mathcomp.analysis.constructive_ereal

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


Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

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.

Local Tactic Notation "elift" constr(lm) ":" ident(x) :=
  by case: x => [||?]; first by rewrite ?eqe; apply: lm.

Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) :=
  by case: x y => [?||] [?||]; first by rewrite ?eqe; apply: lm.

Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) ident(z) :=
  by case: x y z => [?||] [?||] [?||]; first by rewrite ?eqe; apply: lm.

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

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

Local Notation "x +? y" := (adde_def x y).

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] &, forall 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, forall 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))).

Local Notation "x *? y" := (mule_def x y).

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] &, forall x y, x +? y}.

Lemma ltninfty_adde_def : {in [pred x | -oo < x] &, forall 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 (forall 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) :
    (forall 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) :
    (forall 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 &, forall 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) :
    (forall 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) :
  (forall 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 <-> exists 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) = [exists i in P, f i == -oo].

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

Lemma esum_eqy ( I : finType) ( P : {pred I}) ( f : I -> \bar R) :
  (forall i, P i -> f i != -oo) ->
  (\sum_( i | P i) f i == +oo) = [exists 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) :
  (forall t, P t -> 0 <= f t) -> forall l, 0 <= \sum_( i <- l | P i) f i.

Lemma sume_le0 T ( f : T -> \bar R) ( P : pred T) :
  (forall t, P t -> f t <= 0) -> forall 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 <-> exists 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) = [exists i in P, f i == +oo].

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

Lemma desum_eqNy ( I : finType) ( f : I -> \bar R) ( P : {pred I}) :
  (forall i, f i != +oo) ->
  (\sum_( i | P i) f i == -oo) = [exists 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) :
  (forall n, P n -> 0 <= f n) -> forall l, 0 <= \sum_( i <- l | P i) f i.

Lemma dsume_le0 T ( f : T -> \bar R) ( P : pred T) :
  (forall n, P n -> f n <= 0) -> forall 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 <-> (forall 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) : (forall 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) :
  (forall 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) :
  (forall 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], forall 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], forall 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) : (forall 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) : (forall 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) :
  (forall 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) :
  (forall 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 :
  (forall 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 :
  (forall 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 :
  (forall 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 :
  (forall 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], forall 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], forall 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) :
  (forall 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) :
  (forall 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) :
  (forall 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) :
  (forall 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 &, forall 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 : (forall r, r%:E <= x) -> x = +oo.

Lemma eq_ninfty x : (forall 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) :
  (forall 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], forall 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], forall 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) : (forall 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) : (forall 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) :
  (forall 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) :
  (forall 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 :
  (forall 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 :
  (forall 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 :
  (forall 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 :
  (forall 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], forall 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], forall 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) :
  (forall 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) :
  (forall 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) :
  (forall 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) :
  (forall 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 (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).

Lemma lee_subgt0Pr x y :
  reflect (forall e, (0 < e)%R -> x - e%:E <= y) (x <= y).

Lemma lee_mul01Pr x y : 0 <= x ->
  reflect (forall 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 (forall 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}.
Local Notation nR := {compare (0 : \bar R) & nz & cond}.
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}.
Local Notation nR := {compare (0 : \bar R) & nz & r}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : R) nz r).

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}.
Local Notation nR := {compare (0 : \bar R) & ?=0 & >=0}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : \bar R) ?=0 >=0).

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.

Definition expand r : \bar R :=
  if (r >= 1)%R then +oo else if (r <= -1)%R then -oo else (r / (1 - `|r|))%:E.

Lemma expand1 r : (1 <= r)%R -> expand r = +oo.

Lemma expandN r : expand (- r)%R = - expand r.

Lemma expandN1 r : (r <= -1)%R -> expand r = -oo.

Lemma expand0 : expand 0%R = 0.

Lemma expandK : {in [pred r | `|r| <= 1]%R, cancel expand contract}.

Lemma le_contract : {mono contract : x y / (x <= y)%O}.

Definition lt_contract := leW_mono le_contract.
Definition contract_inj := mono_inj lexx le_anti le_contract.

Lemma le_expand_in : {in [pred r | `|r| <= 1]%R &,
  {mono expand : x y / (x <= y)%O}}.

Definition lt_expand := leW_mono_in le_expand_in.
Definition expand_inj := mono_inj_in lexx le_anti le_expand_in.

Lemma fine_expand r : (`|r| < 1)%R ->
  (fine (expand r))%:E = expand r.

Lemma le_expand : {homo expand : x y / (x <= y)%O}.

Lemma expand_eqoo r : (expand r == +oo) = (1 <= r)%R.

Lemma expand_eqNoo r : (expand r == -oo) = (r <= -1)%R.

End contract_expand.

Section ereal_PseudoMetric .
Variable R : realFieldType.
Implicit Types (x y : \bar R) (r : R).

Definition ereal_ball x r y := (`|contract x - contract y| < r)%R.

Lemma ereal_ball_center x r : (0 < r)%R -> ereal_ball x r x.

Lemma ereal_ball_sym x y r : ereal_ball x r y -> ereal_ball y r x.

Lemma ereal_ball_triangle x y z r1 r2 :
  ereal_ball x r1 y -> ereal_ball y r2 z -> ereal_ball x (r1 + r2) z.

Lemma ereal_ballN x y ( e : {posnum R}) :
  ereal_ball (- x) e%:num (- y) -> ereal_ball x e%:num y.

Lemma ereal_ball_ninfty_oversize ( e : {posnum R}) x :
  (2 < e%:num)%R -> ereal_ball -oo e%:num x.

Lemma contract_ereal_ball_pinfty r ( e : {posnum R}) :
  (1 < contract r%:E + e%:num)%R -> ereal_ball r%:E e%:num +oo.

End ereal_PseudoMetric.

Lemma lt_ereal_nbhs ( R : realFieldType) ( a b : \bar R) ( r : R) :
  a < r%:E -> r%:E < b ->
  exists delta : {posnum R},
    forall y, (`|y - r| < delta%:num)%R -> (a < y%:E) && (y%:E < b).