Module mathcomp.reals.constructive_ereal

From HB Require Import structures.
From mathcomp Require Import boot order algebra finmap interval_inference.

# Extended real numbers $\overline{R}$ Given a type R for numbers, `\bar R` is the type `R` extended with symbols `-oo` and `+oo` (notation scope: `%E`), suitable to represent extended real numbers. When `R` is a `numDomainType`, `\bar R` is equipped with a canonical `porderType` and operations for addition/opposite. When `R` is a `realDomainType`, `\bar R` is equipped with a canonical `orderType`. Naming convention: in definition/lemma identifiers, "e" stands for an extended number and "y" and "Ny" for `+oo` and `-oo` respectively. Examples of notations: | Coq definitions | | Meaning | |-----------------------:|--|--------------------------------------------| | `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$| | | | notation for `extended (R:Type)` | | `r%:E` |==| injects real numbers into `\bar R` | | - x |==| opposite of x : \bar R | | 0, 1, -1 |==| 0%R, 1%R%:E, - 1%R%:E | | <number> |==| <number>%:R%:E with <number> a sequence | | | | of digits | | -<number> |==| - <number>%:R%:E with <number> a sequence | | | | of digits | | `+%E, -%E, *%E` |==| addition/opposite/multiplication for | | | | extended reals | | `x^-1`, `x / y` |==| inverse and division for extended reals | | `er_map (f : T -> T')` |==| the `\bar T -> \bar T'` lifting of `f` | | `sqrte` |==| square root for extended reals | | `` `\| x \|%E `` |==| the absolute value of `x` | | `x ^+ n` |==| iterated multiplication | | `x *+ n` |==| iterated addition | | `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition | | | | ($-\infty + +\infty = +\infty$) | | | | Import DualAddTheory for related lemmas | | `x +? y` |==| the addition of `x` and `y` is defined | | | | it is neither $+\infty - \infty$ | | | | nor $-\infty + \infty$ | | `x *? y` |==| the multiplication of `x` and `y` is not | | | | of the form $0 * +\infty$ or $0 * -\infty$ | | `x *^-1? y` |==| the inverse commutes with the product | | `(_ <= _)%E`, `(_ < _)%E`,|==| comparison relations for extended reals | | `(_ >= _)%E`, `(_ > _)%E` | | | | `(\sum_(i in A) f i)%E`|==| bigop-like notation in scope `%E` | |`(\prod_(i in A) f i)%E`|==| bigop-like notation in scope `%E` | | `maxe x y, mine x y` |==| notation for the maximum/minimum | Detailed documentation: ``` \bar R == coproduct of R and {+oo, -oo}; notation for extended (R:Type) r%:E == injects real numbers into \bar R - x == opposite of x : \bar R 0, 1, -1 == 0%R, 1%R%:E, - 1%R%:E <number> == <number>%:R%:E with <number> a sequence of digits -<number> == - <number>%:R%:E with <number> a sequence of digits +%E, -%E, *%E == addition/opposite/multiplication for extended reals x^-1, x / y == inverse and division for extended reals er_map (f : T -> T') == the \bar T -> \bar T' lifting of f sqrte == square root for extended reals `| x |%E == the absolute value of x x ^+ n == iterated multiplication x *+ n == iterated addition +%dE, (x *+ n)%dE == dual addition/dual iterated addition for extended reals (-oo + +oo = +oo instead of -oo) Import DualAddTheory for related lemmas x +? y == the addition of the extended real numbers x and and y is defined, i.e., it is neither +oo - oo nor -oo + oo x *? y == the multiplication of the extended real numbers x and y is not of the form 0 * +oo or 0 * -oo x *^-1? y == the inverse commutes with the product (_ <= _)%E, (_ < _)%E, == comparison relations for extended reals (_ >= _)%E, (_ > _)%E (\sum_(i in A) f i)%E == bigop-like notation in scope %E (\prod_(i in A) f i)%E == bigop-like notation in scope %E maxe x y, mine x y == notation for the maximum/minimum of two extended real numbers esg x == sign of x (0, -1, or +1, as an extended real) ``` ## Signed extended real numbers ``` {posnum \bar R} == interface type for elements in \bar R that are positive, c.f., interval_inference.v, notation in scope %E {nonneg \bar R} == interface types for elements in \bar R that are non-negative, c.f. interval_inference.v, notation in scope %E x%:pos == explicitly casts x to {posnum \bar R}, in scope %E x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E ``` ## Topology of extended real numbers ``` contract == order-preserving bijective function from extended real numbers to [-1; 1] expand == function from real numbers to extended real numbers that cancels contract in [-1; 1] ```

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

Reserved Notation "x %:E" (format "x %:E").
Reserved Notation "x %:dE" (format "x %:dE").
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 "'\bar' '^d' x" (at level 2, format "'\bar' '^d' 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 ( : Type) := of R | | .
Arguments EFin {R}.

Lemma : injective (@EFin T).

Proof.

by move=> a b; case. Qed.

Definition := extended.

Definition : forall {}, R -> dual_extended R := @EFin.

Notation := (@EPInf _ : dual_extended _) : ereal_dual_scope.
Notation := (@EPInf _) : ereal_scope.
Notation := (@ENInf _ : dual_extended _) : ereal_dual_scope.
Notation := (@ENInf _) : ereal_scope.
Notation := (@EFin _ r%R : dual_extended _) : ereal_dual_scope.
Notation := (@EFin _ r%R : dual_extended _) : ereal_dual_scope.
Notation := (@EFin _ r%R).
Notation := (extended R) : type_scope.
Notation := (dual_extended R) : type_scope.
Notation := (@GRing.zero (\bar^d _)) : ereal_dual_scope.
Notation := (@GRing.zero (\bar _)) : ereal_scope.
Notation := (1%R%:E : dual_extended _) : ereal_dual_scope.
Notation := (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 ( : T -> T') ( : \bar T) : \bar T' :=
  match x with
  | r%:E => (f r)%:E
  | +oo => +oo
  | -oo => -oo
  end.

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

Proof.

by case: x. Qed.

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

Section EqEReal.
Variable ( : eqType).

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

Lemma : Equality.axiom eq_ereal.

Proof.

by case=> [?||][?||]; apply: (iffP idP) => //= [/eqP|[]] ->. Qed.

..Build (\bar R) ereal_eqP.

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

Proof.

by []. Qed.

End EqEReal.

Section ERealChoice.
Variable ( : choiceType).

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

Definition ( : 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 : pcancel code decode

Proof.

by case. Qed.

..copy (\bar R) (pcan_type codeK).

End ERealChoice.

Section ERealCount.
Variable ( : countType).

. (@codeK R).

End ERealCount.

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

Definition :=
  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 :=
  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_ereal x y = (y != x) && le_ereal x y.

Proof.

by case: x y => [?||][?||] //=; rewrite lt_def eqe. Qed.

Lemma : reflexive le_ereal.

Proof.

by case => /=. Qed.

Lemma : ssrbool.antisymmetric le_ereal.

Proof.

by case=> [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed.

Lemma : ssrbool.transitive le_ereal.

Proof.

case=> [?||][?||][?||] //=; rewrite -?comparabler0; first exact: le_trans.
by move=> /le_comparable cmp /(comparabler_trans cmp).
by move=> cmp /ge_comparable /comparabler_trans; apply.
Qed.

Fact : Order.disp_t

Proof.

by []. Qed.

..isPOrder.Build ereal_display (\bar R)
lt_def_ereal le_refl_ereal le_anti_ereal le_trans_ereal.

Lemma : (x <= y)%O = le_ereal x y

Proof.

by []. Qed.

Lemma : (x < y)%O = lt_ereal x y

Proof.

by []. Qed.

End ERealOrder.

Notation := (@Order.le ereal_display _) (only parsing).
Notation :=
  (@Order.le ereal_display R) (at level 10, R at level 8, only parsing).
Notation := (@Order.lt ereal_display _) (only parsing).
Notation :=
  (@Order.lt ereal_display R) (at level 10, R at level 8, only parsing).
Notation := (@Order.ge ereal_display _) (only parsing).
Notation :=
  (@Order.ge ereal_display R) (at level 10, R at level 8, only parsing).
Notation := (@Order.gt ereal_display _) (only parsing).
Notation :=
  (@Order.gt ereal_display R) (at level 10, R at level 8, only parsing).

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

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

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

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

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

Section ERealZsemimodule.
Context { : nmodType}.
Implicit Types x y z : \bar R.

Definition :=
  match x, y with
  | x%:E , y%:E  => (x + y)%:E
  | -oo, _     => -oo
  | _    , -oo => -oo
  | +oo, _     => +oo
  | _    , +oo => +oo
  end.
Arguments adde : simpl never.

Definition :=
  match x, y with
  | x%:E , y%:E  => (x + y)%R%:E
  | +oo, _     => +oo
  | _    , +oo => +oo
  | -oo, _     => -oo
  | _    , -oo => -oo
  end.
Arguments dual_adde : simpl never.

Lemma : associative (S := \bar R) adde.

Proof.

by case=> [x||] [y||] [z||] //; rewrite /adde /= addrA. Qed.

Lemma : commutative (S := \bar R) adde.

Proof.

by case=> [x||] [y||] //; rewrite /adde /= addrC. Qed.

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

Proof.

by case=> // r; rewrite /adde /= add0r. Qed.

..isNmodule.Build (\bar R)
addeA_subproof addeC_subproof add0e_subproof.

Lemma : associative (S := \bar^d R) dual_adde.

Proof.

by case=> [x||] [y||] [z||] //; rewrite /dual_adde /= addrA. Qed.

Lemma : commutative (S := \bar^d R) dual_adde.

Proof.

by case=> [x||] [y||] //; rewrite /dual_adde /= addrC. Qed.

Lemma : left_id (0%:dE%dE : \bar^d R) dual_adde.

Proof.

by case=> // r; rewrite /dual_adde /= add0r. Qed.

..on (\bar^d R).
..isNmodule.Build (\bar^d R)
daddeA_subproof daddeC_subproof dadd0e_subproof.

Definition : \bar R := iterop n +%R x 0.

Definition ( : \bar^d R) : \bar^d R := iterop n +%R x 0.

End ERealZsemimodule.
Arguments adde : simpl never.
Arguments dual_adde : simpl never.

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

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

Lemma : 0 <= 1 :> \bar R

Proof.

by rewrite lee_fin. Qed.

Lemma : 0 < 1 :> \bar R

Proof.

by rewrite lte_fin. Qed.

Lemma : (x <= -oo) = (x == -oo)

Proof.

by case: x. Qed.

Lemma : (+oo <= x) = (x == +oo)

Proof.

by case: x. Qed.

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

Proof.

exact: real0. Qed.

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

Proof.

exact: real0. Qed.

Lemma : (0 : \bar R) <= +oo

Proof.

exact: real0. Qed.

Lemma : -oo <= (0 : \bar R)

Proof.

exact: real0. Qed.

Lemma : ((0 : \bar R) >=< +oo%E)%O.

Proof.

by rewrite /Order.comparable le0y. Qed.

Lemma : ((0 : \bar R) >=< -oo%E)%O.

Proof.

by rewrite /Order.comparable leNy0 orbT. Qed.

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

Proof.

by case: x => [r| |]//; rewrite lte_fin lee_fin lt0r. Qed.

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

Proof.

move: x y => [x||] [y||] //; rewrite /Order.comparable !lee_fin -!realE.
- exact: real_comparable.
- by rewrite /lee/= => ->.
- by rewrite /lee/= => _ ->.
Qed.

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

Proof.

by []. Qed.

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

Proof.

by []. Qed.

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

Proof.

by case: x => //=; rewrite real0. Qed.

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

Proof.

by case: x => //=; rewrite real0. Qed.

Lemma : left_id (+oo : \bar R) Order.min.

Proof.

by case. Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> Order.min x +oo = x.

Proof.

by case: x => [x |//|//] rx; rewrite minEle real_leey [_ \in Num.real]rx.
Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> Order.min -oo%E x = -oo%E.

Proof.

by case: x => [x |//|//] rx; rewrite minEle real_leNye [_ \in Num.real]rx.
Qed.

Lemma : right_zero (-oo : \bar R) Order.min.

Proof.

by case=> [x |//|//]; rewrite minElt. Qed.

Lemma : left_zero (+oo : \bar R) Order.max.

Proof.

by case. Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> Order.max x +oo = +oo.

Proof.

by case: x => [x |//|//] rx; rewrite maxEle real_leey [_ \in Num.real]rx.
Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> Order.max -oo%E x = x.

Proof.

by case: x => [x |//|//] rx; rewrite maxEle real_leNye [_ \in Num.real]rx.
Qed.

Lemma : right_id (-oo : \bar R) Order.max.

Proof.

by case=> [x |//|//]; rewrite maxElt. Qed.

Lemma : 0 <= x <-> x = +oo \/ exists2 , (r >= 0)%R & x = r%:E.

Proof.

Lemma : fine 0 = 0%R :> R

Proof.

by []. Qed.

Lemma : fine 1 = 1%R :> R

Proof.

by []. Qed.

End ERealOrder_numDomainType.

#[global] Hint Resolve lee01 lte01 : core.

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

Lemma : r%:E < +oo

Proof.

exact: num_real. Qed.

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

Proof.

by case: x => // r; rewrite ltry. Qed.

Lemma : -oo < r%:E

Proof.

exact: num_real. Qed.

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

Proof.

by case: x => // r; rewrite ltNyr. Qed.

Lemma : x <= +oo

Proof.

by case: x => //= r; exact: num_real. Qed.

Lemma : -oo <= x

Proof.

by case: x => //= r; exact: num_real. Qed.

Definition := (ltey, leey).

Definition := (ltNye, leNye).

Lemma ( : R -> R) : {homo f : / (x <= y)%R} ->
{homo er_map f : / x <= y}.

Proof.

move=> ndf.
by move=> [r| |] [l| |]//=; rewrite ?leey ?leNye// !lee_fin; exact: ndf.
Qed.

Lemma : total (Order.le : rel (\bar R)).

Proof.

by move=> [?||][?||]//=; rewrite (ltEereal, leEereal)/= ?num_real ?le_total.
Qed.

..POrder_isTotal.Build ereal_display (\bar R)
  le_total_ereal.

..hasBottom.Build ereal_display (\bar R) leNye.
..hasTop.Build ereal_display (\bar R) leey.

End ERealOrder_realDomainType.

Section ERealZmodule.
Context { : zmodType}.
Implicit Types x y z : \bar R.

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

End ERealZmodule.

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

Definition :=
  match x, y with
  | x%:E , y%:E => (x * y)%:E
  | +oo, +oo | -oo, -oo => +oo
  | +oo, -oo | -oo, +oo => -oo
  | -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.
Arguments mule : simpl never.

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

Definition :=
  match x with
  | x%:E => if x == 0%R then +oo else (x^-1)%:E
  | +oo => 0
  | -oo => -oo
  end.
Arguments inve : simpl never.

Definition := iterop n mule x 1.

End ERealArith.
Arguments mule : simpl never.
Arguments inve : simpl never.

Elpi Command canonical_notation_ereal.
Elpi Accumulate lp:{{ /**/  }}.
Elpi .
Elpi Command canonical_notation_dual_ereal.
Elpi Accumulate lp:{{ /**/  }}.
Elpi .

Local Notation := (@GRing.add (\bar^d _)).
Local Notation := (@GRing.add (@reverse_coercion _ _ _ (\bar^d _))).
Local Notation := (@GRing.add dual_extended_nmodType).
Local Notation := (@GRing.add (\bar _)).
Local Notation := (@GRing.add (@reverse_coercion _ _ _ (\bar _))).
Local Notation := (@GRing.add extended_nmodType).

Notation := add_parsingde (only parsing).
Notation := add_rcde (only printing).
Notation := add_cande (only printing).
Notation   := add_parsinge (only parsing).
Notation   := add_rce (only printing).
Notation   := add_cane (only printing).
Notation   := oppe.
Notation := (add_parsingde x%dE y%dE) (only parsing) : ereal_dual_scope.
Notation := (add_rcde x%dE y%dE) (only printing) : ereal_dual_scope.
Notation := (add_cande x%dE y%dE) (only printing) : ereal_dual_scope.
Notation := (add_parsinge x%E y%E) (only parsing) : ereal_scope.
Notation := (add_rce x%E y%E) (only printing) : ereal_scope.
Notation := (add_cane x%E y%E) (only printing) : ereal_scope.
Notation := (add_parsingde x%dE (oppe (y%dE : \bar^d _))%dE)
  (only parsing) : ereal_dual_scope.
Notation := (add_rcde x%dE (oppe y%dE))
  (only printing) : ereal_dual_scope.
Notation := (add_cande x%dE (oppe y%dE))
  (only printing) : ereal_dual_scope.
Notation := (add_parsinge x%E (oppe y%E)) (only parsing) : ereal_scope.
Notation := (add_rce x%E (oppe y%E)) (only printing) : ereal_scope.
Notation := (add_cane x%E (oppe y%E)) (only printing) : ereal_scope.

Notation    := (oppe (x%dE : \bar^d _)) : ereal_dual_scope.
Notation    := (oppe x%E) : ereal_scope.
Notation    := mule.
Notation := (mule x%dE y%dE : \bar^d _) : ereal_dual_scope.
Notation := (mule x%E y%E) : ereal_scope.
Notation := (abse x%dE : \bar^d _) : ereal_dual_scope.
Notation := (abse x%E) : ereal_scope.
Notation := (inve x%dE : \bar^d _) : ereal_dual_scope.
Notation := (inve x) : ereal_scope.
Notation := (mule x%dE (inve y%dE) : \bar^d _) : ereal_dual_scope.
Notation := (mule x (inve y)) : ereal_scope.
Arguments abse {R}.
Notation := (expe x%dE n : \bar^d _) : ereal_dual_scope.
Notation := (expe x%E n) : ereal_scope.
Notation := (ednatmul x%dE n) : ereal_dual_scope.
Notation := (enatmul x%E n) : ereal_scope.

Notation for constant numerals. This has been introduced so that, e.g., in the scope `ereal_scope`, `-<n>` is correctly parsed without requiring one writes `- <n>%:E`. See the Rocq reference manual for the `Number Notation` command and [PR #1704](https://github.com/math-comp/analysis/pull/1704) for more explanations.

Variant := : Ione.
Inductive := : Ione -> nat -> Inatmul.
Inductive := : Inatmul -> IEFin | : IEFin -> IEFin.
Variant :=.

Definition ( : Number.int) : IEFin :=
  match x with
  | Number.IntDecimal (Decimal.Pos u) => IEFinP (INatmul IOne (Nat.of_uint u))
  | Number.IntDecimal (Decimal.Neg u) =>
      IEFinN (IEFinP (INatmul IOne (Nat.of_uint u)))
  | Number.IntHexadecimal (Hexadecimal.Pos u) =>
      IEFinP (INatmul IOne (Nat.of_hex_uint u))
  | Number.IntHexadecimal (Hexadecimal.Neg u) =>
      IEFinN (IEFinP (INatmul IOne (Nat.of_hex_uint u)))
  end.

Definition ( : IEFin) : option Number.int :=
  match x with
  | IEFinP (INatmul IOne n) =>
      Some (Number.IntDecimal (Decimal.Pos (Nat.to_uint n)))
  | IEFinN (IEFinP (INatmul IOne n)) =>
      Some (Number.IntDecimal (Decimal.Neg (Nat.to_uint n)))
  | _ => None
  end.

Arguments GRing.one {_}.
#[warnings="-via-type-remapping,-via-type-mismatch"]
Number Notation Idummy_placeholder parse print (via IEFin
  mapping [[EFin] => IEFinP, [oppe] => IEFinN,
           [GRing.natmul] => INatmul, [GRing.one] => IOne])
  : ereal_scope.
#[warnings="-via-type-remapping,-via-type-mismatch"]
Number Notation Idummy_placeholder parse print (via IEFin
  mapping [[EFin] => IEFinP, [oppe] => IEFinN,
           [GRing.natmul] => INatmul, [GRing.one] => IOne])
  : ereal_dual_scope.
Arguments GRing.one : clear implicits.

Notation := (oppe 1 : dual_extended _) : ereal_dual_scope.
Notation := (oppe 1) : ereal_scope.

Notation := (fun => - f x)%dE : ereal_dual_scope.
Notation := (fun => - f x)%E : ereal_scope.
Notation := (fun => add_parsingde (f x)%dE (g x)%dE) (only parsing) : ereal_dual_scope.
Notation := (fun => add_rcde (f x)%dE (g x)%dE) (only printing) : ereal_dual_scope.
Notation := (fun => add_cande (f x)%dE (g x)%dE) (only printing) : ereal_dual_scope.
Notation := (fun => add_parsinge (f x)%E (g x)%E) (only parsing) : ereal_scope.
Notation := (fun => add_rce (f x)%E (g x)%E) (only printing) : ereal_scope.
Notation := (fun => add_cane (f x)%E (g x)%E) (only printing) : ereal_scope.
Notation := (fun => add_parsingde ((f x)%dE : \bar^d _) (oppe ((g%dE x) : \bar^d _))%dE)
  (only parsing) : ereal_dual_scope.
Notation := (fun => add_rcde (f x)%dE (oppe (g x)%dE))
  (only printing) : ereal_dual_scope.
Notation := (fun => add_cande (f x)%dE (oppe (g x)%dE))
  (only printing) : ereal_dual_scope.
Notation := (fun => add_parsinge ((f x)%E : \bar _) (oppe (g x)%E)) (only parsing) : ereal_scope.
Notation := (fun => add_rce (f x)%E (oppe (g x)%E)) (only printing) : ereal_scope.
Notation := (fun => add_cane (f x)%E (oppe (g x)%E)) (only printing) : ereal_scope.
Notation := (fun => (f x * g x)%dE) : ereal_dual_scope.
Notation := (fun => (f x * g x)%E) : ereal_scope.

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

Notation :=
  (\big[*%E/1%:E]_( <- r | P%B) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( <- r) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_(m <= < n | P%B) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_(m <= < n) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( | P%B) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_ F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( : t | P%B) F%E) (only parsing) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( : t) F%E) (only parsing) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( < n | P%B) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( < n) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( in A | P%B) F%E) : ereal_scope.
Notation :=
  (\big[*%E/1%:E]_( in A) F%E) : ereal_scope.

Section ERealOrderTheory.
Context { : 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 : (0 <= (-1)%:E :> \bar R) = false.

Proof.

by rewrite lee_fin ler0N1. Qed.

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

Proof.

by rewrite lte_fin ltr0N1. Qed.

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

Proof.

by rewrite lte_fin ltrN10. Qed.

Lemma : -1 <= 0 :> \bar R.

Proof.

by rewrite lee_fin lerN10. Qed.

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

Proof.

by rewrite lte_fin ltr0n. Qed.

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

Proof.

by rewrite lee_fin ler0n. Qed.

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

Proof.

by rewrite lte_fin ltr1n. Qed.

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

Proof.

by rewrite lee_fin ler1n. Qed.

Lemma : 0 <= x -> (0 <= fine x)%R.

Proof.

by case: x. Qed.

Lemma : 0 < x < +oo -> (0 < fine x)%R.

Proof.

by move: x => [x| |] //=; rewrite ?ltxx ?andbF// lte_fin => /andP[]. Qed.

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

Proof.

by move: x => [x| |] //= /andP[_]; rewrite lte_fin. Qed.

Lemma : x <= 0 -> (fine x <= 0)%R.

Proof.

by case: x. Qed.

Lemma ( : R) : (r0 <= r1)%R -> r0%:E <= r1%:E.

Proof.

by []. Qed.

Lemma ( : R) : (r0 < r1)%R -> r0%:E < r1%:E.

Proof.

by []. Qed.

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

Proof.

by elim: n => //= n ->. Qed.

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

Proof.

by elim: n => //= n ->. Qed.

Lemma : x *+ 0 = 0

Proof.

by []. Qed.

Lemma : x *+ 2 = x + x

Proof.

by []. Qed.

Lemma : x ^+ 0 = 1

Proof.

by []. Qed.

Lemma : x ^+ 2 = x * x

Proof.

by []. Qed.

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

Proof.

move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !lerN2.
by rewrite /Order.le/= realN.
by rewrite /Order.le/= realN.
Qed.

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

Proof.

move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltrN2.
by rewrite /Order.lt/= realN.
by rewrite /Order.lt/= realN.
Qed.

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

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

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

Proof.

by []. Qed.

Lemma : reflect (exists , x = r%:E) (x \in fin_num).

Proof.

by case: x => [r'||]//=; constructor; [exists r'| case | case ]. Qed.

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

Proof.

by []. Qed.

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

Proof.

by apply/(iffP idP) => [/andP//|/andP]. Qed.

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

Proof.

by rewrite fin_numE negb_and ?negbK. Qed.

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

Proof.

by rewrite fin_numEn; apply: (iffP orP) => -[]/eqP; by [left|right]. Qed.

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

Proof.

by move=> /andP[oox xoo]; rewrite fin_numE gt_eqF ?lt_eqF. Qed.

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

Proof.

by rewrite fin_numE; case: x => // r; rewrite real_ltry normr_real. Qed.

End finNumPred.

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

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

Proof.

by move=> [? [?| |]| |]. Qed.

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

Proof.

by move=> [? [?| |]| |]. Qed.

Lemma : `|r%:E|%E = `|r|%:E.

Proof.

by []. Qed.

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

Proof.

by case. Qed.

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

Proof.

by case: x. Qed.

Lemma : x \is a fin_num -> (fine x == 0%R) = (x == 0).

Proof.

by move: x => [//| |] /=; rewrite fin_numE. Qed.

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

Proof.

by []. Qed.

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

Proof.

by case: x => //=; rewrite oppr0. Qed.

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

Proof.

by []. Qed.

Let : @nmod_morphism _ (\bar R) EFin

Proof.

by split. Qed.

..isNmodMorphism.Build R (\bar R) EFin
EFin_semi_additive.

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

Proof.

by []. Qed.

Lemma : (r * r')%:E = r%:E * r'%:E

Proof.

by []. Qed.

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

Proof.

exact: raddfMn. Qed.

Lemma ( : pred T) ( : T -> R) :
\prod_( <- s | P i) (f i)%:E = (\prod_( <- s | P i) f i)%:E.

Proof.

by elim/big_ind2 : _ => // ? x ? y -> ->; rewrite EFinM. Qed.

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

Proof.

exact/esym/raddf_sum. Qed.

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

Proof.

by move=> x y; rewrite !minElt lte_fin -fun_if. Qed.

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

Proof.

by move=> x y; rewrite !maxElt lte_fin -fun_if. Qed.

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

Local Notation := (adde_def x y).

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

Proof.

by rewrite /adde_def andbC (andbC (x == -oo)) (andbC (x == +oo)). Qed.

Lemma : x \is a fin_num -> x +? y.

Proof.

by move: x y => [x| |] [y | |]. Qed.

Lemma : y \is a fin_num -> x +? y.

Proof.

by rewrite adde_defC; exact: fin_num_adde_defr. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

Lemma : x +? y -> x +? z -> x +? (y + z).

Proof.

by move: x y z => [x||] [y||] [z||]. Qed.

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

Proof.

by case: x. Qed.

Lemma : {in [pred | x >= 0] &, forall , x +? y}.

Proof.

by move=> [x| |] [y| |]. Qed.

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

Proof.

exact: addrC. Qed.

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

Proof.

exact: addr0. Qed.

Lemma : x *+ n.+1 = x + x *+ n.

Proof.

by case: n => //=; rewrite adde0. Qed.

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

Proof.

exact: add0r. Qed.

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

Proof.

exact: addrA. Qed.

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

Proof.

move=> fhi; elim/big_rec : _; first by rewrite fin_num_adde_defl.
by move=> i x Pi fhx; rewrite adde_defDr// fhi.
Qed.

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

Proof.

exact: Monoid.mulmAC. Qed.

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

Proof.

exact: Monoid.mulmCA. Qed.

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

Proof.

exact: Monoid.mulmACA. Qed.

Lemma : 0 < x -> 0 < y -> 0 < x + y.

Proof.

by move: x y => [x| |] [y| |] //; rewrite !lte_fin; exact: addr_gt0.
Qed.

Lemma : 0 <= x -> 0 <= y -> (x + y == 0) = (x == 0) && (y == 0).

Proof.

move: x y => [x| |] [y| |]//; rewrite !lee_fin; first exact: paddr_eq0.
by move=> x0 _ /=; rewrite andbF.
Qed.

Lemma : x <= 0 -> y <= 0 -> (x + y == 0) = (x == 0) && (y == 0).

Proof.

move: x y => [x| |] [y| |]//; rewrite !lee_fin; first exact: naddr_eq0.
by move=> x0 _ /=; rewrite andbF.
Qed.

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

Proof.

case: x y => [x||] [y||] //; exact: realD. Qed.

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

Proof.

by rewrite /= oppr0. Qed.

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

Proof.

by case=> [x||] //=; rewrite opprK. Qed.

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

Proof.

exact: inv_inj oppeK. Qed.

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

Proof.

by rewrite adde_defN oppeK. Qed.

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

Proof.

by rewrite -[RHS](can_eq oppeK) oppe0. Qed.

Lemma : x +? y -> - (x + y) = - x - y.

Proof.

by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed.

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

Proof.

by move=> finy; rewrite oppeD// fin_num_adde_defl. Qed.

Lemma : x - 0 = x.

Proof.

by move: x => [x| |] //; rewrite -EFinB subr0. Qed.

Lemma : 0 - x = - x.

Proof.

by move: x => [x| |] //; rewrite -EFinB sub0r. Qed.

Lemma : x * y = y * x.

Proof.

by move: x y => [r||] [s||]//=; rewrite -EFinM mulrC. Qed.

Lemma : 1 != 0 :> \bar R

Proof.

exact: oner_neq0. Qed.

Lemma : (1 == 0 :> \bar R) = false

Proof.

exact: oner_eq0. Qed.

Lemma : x * 1 = x.

Proof.

by move: x=> [r||]/=; rewrite /mule/= ?mulr1 ?(negbTE onee_neq0) ?lte_tofin.
Qed.

Lemma : 1 * x = x.

Proof.

by rewrite muleC mule1. Qed.

Lemma : x * 0 = 0.

Proof.

by move: x => [r| |] //=; rewrite /mule/= ?mulr0// eqxx. Qed.

Lemma : 0 * x = 0.

Proof.

by move: x => [r| |]/=; rewrite /mule/= ?mul0r// eqxx. Qed.

..isMulLaw.Build (\bar R) 0 mule mul0e mule0.

Lemma : x ^+ n.+1 = x * x ^+ n.

Proof.

by case: n => //=; rewrite mule1. Qed.

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

Proof.

by elim: n => [//|n IHn]; rewrite exprS EFinM IHn expeS. Qed.

Definition :=
  match x, y with
  | _%:E, _%:E | +oo, +oo | -oo, -oo | +oo, -oo | -oo, +oo => true
  | r%:E, _ | _, r%:E => (r != 0%R)
  end.
Arguments mule_def : simpl never.
Local Notation := (mule_def x y).

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

Proof.

by rewrite /mule_def; case: x => [r||]; case: y => [s||]//=;
rewrite ?(andbF, orbF, eqxx, andbT).
Qed.

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

Proof.

by rewrite !mule_defE orbC. Qed.

Lemma : x \is a fin_num -> y \is a fin_num -> x *? y.

Proof.

by case: x y => [r||] [s||]. Qed.

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

Proof.

by case: x y => [?||] [?||]. Qed.

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

Proof.

by case: x y => [?||] [?||]. Qed.

Lemma : x * y != 0 -> x *? y.

Proof.

by move: x y => [x| |] [y| |] //=;
apply: contra_neq => -> //=; rewrite (mule0, mul0e).
Qed.

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

Proof.

by move=> [x| |] [y| |]. Qed.

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

Proof.

by move=> [x| |] [y| |]. Qed.

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

Proof.

by move: x => [| |] //= r; rewrite !eqe normr_eq0. Qed.

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

Proof.

by rewrite /abse/= normr0. Qed.

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

Proof.

by rewrite /abse normr1. Qed.

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

Proof.

by case: x => [r||]; rewrite //= normrN. Qed.

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

Proof.

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

Proof.

by split=> [/eqP | -> //]; rewrite eqe_opp => /eqP. Qed.

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

Proof.

by move: x y => [r0| |] [r1| |] //=; rewrite !eqe eqr_oppLR. Qed.

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

Proof.

split=> /eqP; first by rewrite eqe_oppLR => /eqP.
by rewrite -eqe_oppLR => /eqP.
Qed.

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

Proof.

by rewrite !fin_num_abs abseN. Qed.

Lemma : x +? - y -> - (x - y) = - x + y.

Proof.

by move=> xy; rewrite oppeD// oppeK. Qed.

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

Proof.

by move=> ?; rewrite oppeB// adde_defN fin_num_adde_defl. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

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

Proof.

by rewrite -big_all big_map big_filter; exact: (big_morph _ fin_numD).
Qed.

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

Proof.

rewrite sum_fin_num; apply: (iffP allP) => /=.
by move=> + x xs Px; apply; rewrite map_f// mem_filter Px.
by move=> + _ /mapP[x /[!mem_filter]/andP[Px xs] ->]; apply.
Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

Lemma : x \is a fin_num -> y \is a fin_num ->
x * y \is a fin_num.

Proof.

by move: x y => [x| |] [y| |]. Qed.

Lemma ( : Type) ( : seq I) ( : pred I) ( : I -> \bar R) :
(forall , P i -> f i \is a fin_num) ->
\prod_( <- s | P i) f i \is a fin_num.

Proof.

by move=> ffin; elim/big_ind : _ => // x y x0 y0; rewrite fin_numM. Qed.

Lemma : x \is a fin_num -> x ^+ n \is a fin_num.

Proof.

by elim: n x => // n ih x finx; rewrite expeS fin_numM// ih. Qed.

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

Proof.

by move=> [r| |] [s| |]. Qed.

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

Proof.

by move=> [r| |] [s| |]. Qed.

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

Proof.

by move=> [x| |] [y| |]. Qed.

Lemma : x \is a fin_num -> (fine x)%:E = x.

Proof.

by case: x. Qed.

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

Proof.

by move=> h; rewrite -sumEFin; apply: eq_bigr => i Pi; rewrite fineK// h.
Qed.

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

Proof.

by move=> h; rewrite -EFin_sum_fine. Qed.

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

Proof.

elim: s => [|a b ih h]; first by rewrite !big_nil oppe0.
rewrite !big_cons; case: ifPn => Pa; last by rewrite ih.
by rewrite oppeD ?ih// adde_def_sum// => i Pi; rewrite h.
Qed.

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

Proof.

by move=> h; rewrite sumeN// => i j Pi Pj; rewrite fin_num_adde_defl// h.
Qed.

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

Proof.

move=> nmf nm; under eq_big_nat => i /andP[ni im] do
rewrite -[f i.+1]fineK -1?[f i]fineK ?(nmf, ni, im) 1?ltnW//= -EFinD.
by rewrite sumEFin telescope_sumr// EFinB !fineK ?nmf ?nm ?leqnn.
Qed.

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

Proof.

by move: x y => [x| |] [y| |] //; rewrite -EFinD -EFinB addrK. Qed.

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

Proof.

by move: x y => [x| |] [y| |] //; rewrite -EFinD subrK. Qed.

Lemma : x \is a fin_num -> x - x = 0.

Proof.

by move: x => [r _| |] //; rewrite -EFinB subrr. Qed.

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

Proof.

by move: x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq.
Qed.

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

Proof.

by move: x y => [?| |] [?| |]. Qed.

Lemma : x != -oo -> +oo + x = +oo

Proof.

by case: x. Qed.

Lemma : x != -oo -> x + +oo = +oo

Proof.

by case: x. Qed.

Lemma : -oo + x = -oo

Proof.

by []. Qed.

Lemma : x + -oo = -oo

Proof.

by case: x. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

Lemma : (0 <= x) && (0 <= y) || (x <= 0) && (y <= 0) ->
(x + y == 0) = (x == 0) && (y == 0).

Proof.

by move=> /orP[|] /andP[]; [exact: padde_eq0|exact: nadde_eq0]. Qed.

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

Proof.

split=> [|[i [si Pi fi]]].
  rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|].
  by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo.
rewrite big_mkcond (bigID (xpred1 i))/= (eq_bigr (fun _ => -oo)).
  by move=> j /eqP ->; rewrite Pi.
rewrite big_const_seq/= [X in X + _](_ : _ = -oo)//.
elim: s i Pi fi si => // h t ih i Pi fi.
rewrite inE => /predU1P[<-/=|it]; first by rewrite eqxx.
by rewrite /= iterD ih//=; case: (_ == _).
Qed.

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

Proof.

apply/idP/idP => [/eqP/esum_eqNyP|/existsP[i /andP[Pi /eqP fi]]].
by move=> -[i [_ Pi fi]]; apply/existsP; exists i; rewrite fi eqxx andbT.
by apply/eqP/esum_eqNyP; exists i.
Qed.

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

Proof.

move=> finoo; split=> [|[i [si Pi fi]]].
  rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|].
  by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo.
elim: s i Pi fi si => // h t ih i Pi fi.
rewrite inE => /predU1P[<-/=|it].
  rewrite big_cons Pi fi addye//.
  by apply/eqP => /esum_eqNyP[j [jt /finoo/negbTE/eqP]].
by rewrite big_cons; case: ifPn => Ph; rewrite (ih i)// addey// finoo.
Qed.

Lemma ( : finType) ( : {pred I}) ( : I -> \bar R) :
(forall , P i -> f i != -oo) ->
(\sum_( | P i) f i == +oo) = [exists in P, f i == +oo].

Proof.

move=> fio; apply/idP/existsP => [/eqP /=|[/= i /andP[Pi /eqP fi]]].
have {}fio : (forall , P i -> f i != -oo) by move=> i Pi; exact: fio.
by move=> /(esum_eqyP _ fio)[i [_ Pi fi]]; exists i; rewrite fi eqxx andbT.
by apply/eqP/esum_eqyP => //; exists i.
Qed.

Lemma : 0 <= x -> 0 <= y -> 0 <= x + y.

Proof.

by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed.

Lemma : x <= 0 -> y <= 0 -> x + y <= 0.

Proof.

move: x y => [r0||] [r1||]// ? ?; rewrite !lee_fin -(addr0 0%R); exact: lerD.
Qed.

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

Proof.

move: x => [x||] //; exact: oppr_gt0. Qed.

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

Proof.

move: x => [x||] //; exact: oppr_lt0. Qed.

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

Proof.

move: x => [x||] //; exact: oppr_ge0. Qed.

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

Proof.

move: x => [x||] //; exact: oppr_le0. Qed.

Lemma : (0 >=< - x)%O = (0 >=< x)%O.

Proof.

by rewrite /Order.comparable oppe_ge0 oppe_le0 orbC. Qed.

Lemma ( : T -> \bar R) ( : pred T) :
(forall , P t -> 0 <= f t) -> forall , 0 <= \sum_( <- l | P i) f i.

Proof.

by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_ge0/f0. Qed.

Lemma ( : T -> \bar R) ( : pred T) :
(forall , P t -> f t <= 0) -> forall , \sum_( <- l | P i) f i <= 0.

Proof.

by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_le0/f0. Qed.

Lemma : -oo * +oo = -oo :> \bar R

Proof.

by []. Qed.

Lemma : +oo * -oo = -oo :> \bar R

Proof.

by []. Qed.

Lemma : +oo * +oo = +oo :> \bar R

Proof.

by []. Qed.

Lemma : -oo * -oo = +oo :> \bar R

Proof.

by []. Qed.

Lemma : r \is Num.real -> r%:E * +oo = (Num.sg r)%:E * +oo.

Proof.

move=> rreal; rewrite /mule/= !eqe sgr_eq0; case: ifP => [//|rn0].
move: rreal => /orP[|]; rewrite le_eqVlt.
by rewrite eq_sym rn0/= => rgt0; rewrite lte_fin rgt0 gtr0_sg// lte01.
by rewrite rn0/= => rlt0; rewrite lt_def lt_geF// andbF ltr0_sg// lte0N1.
Qed.

Lemma : r \is Num.real -> +oo * r%:E = (Num.sg r)%:E * +oo.

Proof.

by move=> rreal; rewrite muleC real_mulry. Qed.

Lemma : r \is Num.real -> r%:E * -oo = (Num.sg r)%:E * -oo.

Proof.

Lemma : r \is Num.real -> -oo * r%:E = (Num.sg r)%:E * -oo.

Proof.

by move=> rreal; rewrite muleC real_mulrNy. Qed.

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

Lemma : -1 * x = - x.

Proof.

by case: x => [r| |]/=;
rewrite /mule ?mulN1r// eqe oppr_eq0 oner_eq0/= lte_fin oppr_gt0 ltr10.
Qed.

Lemma : x * -1 = - x

Proof.

by rewrite muleC mulN1e. Qed.

Lemma : x != 0 -> y != 0 -> x * y != 0.

Proof.

move: x y => [x||] [y||] x0 y0 //; rewrite /mule/= ?(lt0y,mulf_neq0)//;
try by (rewrite (negbTE x0); case: ifPn) ||
by (rewrite (negbTE y0); case: ifPn).
Qed.

Lemma : (x * y == 0) = (x == 0) || (y == 0).

Proof.

apply/idP/idP => [|/orP[] /eqP->]; rewrite ?(mule0, mul0e)//.
by apply: contraTT => /norP[]; exact: mule_neq0.
Qed.

Lemma : 0 <= x -> 0 <= y -> 0 <= x * y.

Proof.

move: x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin, lt0y)//.
- exact: mulr_ge0.
- rewrite le_eqVlt => /predU1P[<- _|x0 _]; first by rewrite eqxx.
by rewrite gt_eqF // x0 le0y.
- move=> _; rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite eqxx.
by rewrite gt_eqF // y0 le0y.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I) ( : I -> \bar R) :
(forall , P i -> 0 <= f i) -> 0 <= \prod_( <- s | P i) f i.

Proof.

by move=> f0; elim/big_ind : _ => // x y x0 y0; rewrite mule_ge0. Qed.

Lemma : 0 < x -> 0 < y -> 0 < x * y.

Proof.

by rewrite !lt_def => /andP[? ?] /andP[? ?]; rewrite mule_neq0 ?mule_ge0.
Qed.

Lemma : x <= 0 -> y <= 0 -> 0 <= x * y.

Proof.

move: x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin)//.
- exact: mulr_le0.
- by rewrite lt_leAnge => -> _; case: ifP => _ //; rewrite andbF le0y.
- by rewrite lt_leAnge => _ ->; case: ifP => _ //; rewrite andbF le0y.
Qed.

Lemma : x <= 0 -> 0 <= y -> x * y <= 0.

Proof.

move: x y => [x| |] [y| |] //; rewrite /mule/= ?(lee_fin, lte_fin).
- exact: mulr_le0_ge0.
- by move=> x0 _; case: ifP => _ //; rewrite lt_leAnge /= x0 andbF leNy0.
- move=> _; rewrite le_eqVlt => /predU1P[<-|->]; first by rewrite eqxx.
by case: ifP => _ //; rewrite leNy0.
Qed.

Lemma : 0 <= x -> y <= 0 -> x * y <= 0.

Proof.

by move=> x0 y0; rewrite muleC mule_le0_ge0. Qed.

Lemma : x < 0 -> y < 0 -> 0 < x * y.

Proof.

by rewrite !lt_neqAle => /andP[? ?]/andP[*]; rewrite eq_sym mule_neq0 ?mule_le0.
Qed.

Lemma : 0 < x -> y < 0 -> x * y < 0.

Proof.

rewrite lt_def !lt_neqAle => /andP[? ?]/andP[? ?].
by rewrite mule_neq0 ?mule_ge0_le0.
Qed.

Lemma : x < 0 -> 0 < y -> x * y < 0.

Proof.

by move=> x0 y0; rewrite muleC mule_gt0_lt0. Qed.

Lemma : 0 < x -> - x < x.

Proof.

by case: x => //= r; rewrite !lte_fin; apply: gtrN. Qed.

Lemma : (0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x * y)%O.

Proof.

case: x y => [x||] [y||]// rx ry;
  do ?[exact: realM
      |by rewrite /mule/= lt0y
      |by rewrite real_mulr_infty ?realE -?lee_fin// /Num.sg;
          case: ifP; [|case: ifP]; rewrite ?mul0e /Order.comparable ?lexx;
          rewrite ?mulN1e ?leNy0 ?mul1e ?le0y
      |by rewrite mulNyNy /Order.comparable le0y].
Qed.

Lemma ( : \bar R) : (0 >=< x)%O = (fine x \in Num.real).

Proof.

by case: x => [x //||//]; rewrite /= real0 /Order.comparable le0y. Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> (0 >=< y)%O ->
x * - y = - (x * y).

Proof.

rewrite !real_fine; case: x y => [x||] [y||] /= xr yr; rewrite /mule//=.
- by rewrite mulrN.
- by case: ifP; rewrite ?oppe0//; case: ifP.
- by case: ifP; rewrite ?oppe0//; case: ifP.
- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin.
by case: (real_ltgtP xr yr) => // <-; rewrite eqxx.
- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin.
by case: (real_ltgtP xr yr) => // <-; rewrite eqxx.
Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> (0 >=< y)%O ->
- x * y = - (x * y).

Proof.

by move=> rx ry; rewrite muleC real_muleN 1?muleC. Qed.

Lemma ( : \bar R) : (0 >=< x)%O -> (0 >=< y)%O ->
- x * - y = x * y.

Proof.

by move=> rx ry; rewrite real_muleN ?real_mulNe ?oppeK ?oppe_cmp0. Qed.

Lemma : x + y \is a fin_num ->
(x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2.

Proof.

case: x y => [x||] [y||] // _.
by rewrite -EFinM -EFin_natmul -!EFin_expe -!EFinD sqrrD.
Qed.

Lemma : 0 <= `|x|.

Proof.

by move: x => [x| |] /=; rewrite ?le0y ?lee_fin. Qed.

Lemma : 0 <= x -> `|x| = x.

Proof.

by move: x => [x| |]//; rewrite lee_fin => x0; apply/eqP; rewrite eqe ger0_norm.
Qed.

Lemma : 0 < x -> `|x| = x

Proof.

by move=> /ltW/gee0_abs. Qed.

Lemma : x <= 0 -> `|x| = - x.

Proof.

by move: x => [x| |]//; rewrite lee_fin => x0; apply/eqP; rewrite eqe ler0_norm.
Qed.

Lemma : x < 0 -> `|x| = - x.

Proof.

by move=> /ltW/lee0_abs. Qed.

Lemma : (x ^+ n == 0) = (n > 0)%N && (x == 0).

Proof.

by elim: n => [|n ih]; rewrite ?expeS ?mule_eq0 ?ih ?andKb// gt_eqF. Qed.

Lemma : 0 < x -> 0 < x ^+ n.

Proof.

by elim: n => //n ih /[dup] /ih xn0 x0; rewrite expeS mule_gt0. Qed.

Lemma : 0 <= x -> 0 <= x ^+ n.

Proof.

by elim: n => // n ih x0; rewrite expeS mule_ge0// ih. Qed.

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

Notation := (@Order.max ereal_display _).
Notation := (@Order.max ereal_display R)
(at level 10, R at level 8, only parsing) : function_scope.

Notation := (@Order.min ereal_display _).
Notation := (@Order.min ereal_display R)
(at level 10, R at level 8, only parsing) : function_scope.

Module .

Section DualERealArithTh_numDomainType.

Local Open Scope ereal_dual_scope.

Context { : numDomainType}.

Implicit Types x y z : \bar^d R.

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

Proof.

by case: x => [x| |]; case: y => [y| |] //=; rewrite opprD !opprK. Qed.

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

Proof.

apply: (big_ind2 (fun => x = - y)%E) => [|_ x _ y -> ->|i _].
- by rewrite oppe0.
- by rewrite dual_addeE !oppeK.
- by rewrite oppeK.
Qed.

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

Proof.

by case: x => [x| |]; case: y. Qed.

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

Proof.

by []. Qed.

Lemma ( : R) : dEFin r = r%:E

Proof.

by []. Qed.

Let : @nmod_morphism _ (\bar^d R) dEFin.

Proof.

by split. Qed.

..isNmodMorphism.Build R (\bar^d R) dEFin
dEFin_semi_additive.

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

Proof.

by []. Qed.

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

Proof.

by rewrite dual_sumeE fin_num_sumeN// oppeK sumEFin. Qed.

Lemma : commutative (S := \bar^d R) +%dE

Proof.

exact: addrC. Qed.

Lemma : right_id (0 : \bar^d R) +%dE

Proof.

exact: addr0. Qed.

Lemma : left_id (0 : \bar^d R) +%dE

Proof.

exact: add0r. Qed.

Lemma : associative (S := \bar^d R) +%dE

Proof.

exact: addrA. Qed.

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

Proof.

exact: Monoid.mulmAC. Qed.

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

Proof.

exact: Monoid.mulmCA. Qed.

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

Proof.

exact: Monoid.mulmACA. Qed.

Lemma : (0%dE >=< x)%O -> (0%dE >=< y)%O -> (0%dE >=< x + y)%O.

Proof.

case: x y => [x||] [y||] //; exact: realD. Qed.

Lemma : x +? y -> - (x + y) = - x - y.

Proof.

by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed.

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

Proof.

by move=> finy; rewrite doppeD// fin_num_adde_defl. Qed.

Lemma : x - 0 = x.

Proof.

by move: x => [x| |] //; rewrite -dEFinB subr0. Qed.

Lemma : 0 - x = - x.

Proof.

by move: x => [x| |] //; rewrite -dEFinB sub0r. Qed.

Lemma : x +? - y -> - (x - y) = - x + y.

Proof.

by move=> xy; rewrite doppeD// oppeK. Qed.

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

Proof.

by move=> ?; rewrite doppeB// fin_num_adde_defl// fin_numN. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

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

Proof.

by move=> [r| |] [s| |]. Qed.

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

Proof.

by move=> [r| |] [s| |]. Qed.

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

Proof.

by move=> fx; rewrite !dual_addeE oppeK addeK ?oppeK; case: x fx. Qed.

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

Proof.

by move=> fy; rewrite !dual_addeE oppeK subeK ?oppeK; case: y fy. Qed.

Lemma : x \is a fin_num -> x - x = 0.

Proof.

by move=> fx; rewrite dual_addeE subee ?oppe0; case: x fx. Qed.

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

Proof.

by move: x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq.
Qed.

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

Proof.

by move: x y => [?| |] [?| |]. Qed.

Lemma : +oo + x = +oo

Proof.

by []. Qed.

Lemma : x + +oo = +oo

Proof.

by case: x. Qed.

Lemma : x != +oo -> -oo + x = -oo

Proof.

by case: x. Qed.

Lemma : x != +oo -> x + -oo = -oo

Proof.

by case: x. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

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

Proof.

by move: x y => [x| |] [y| |]. Qed.

Lemma : x <= 0 -> y <= 0 -> (x + y == 0) = (x == 0) && (y == 0).

Proof.

move: x y => [x||] [y||] //.
- by rewrite !lee_fin -dEFinD !eqe; exact: naddr_eq0.
- by rewrite /adde/= (_ : (-oo == 0) = false)// andbF.
Qed.

Lemma : 0 <= x -> 0 <= y -> (x + y == 0) = (x == 0) && (y == 0).

Proof.

move: x y => [x||] [y||] //.
- by rewrite !lee_fin -dEFinD !eqe; exact: paddr_eq0.
- by rewrite /adde/= (_ : (+oo == 0) = false)// andbF.
Qed.

Lemma : (0 <= x) && (0 <= y) || (x <= 0) && (y <= 0) ->
(x + y == 0) = (x == 0) && (y == 0).

Proof.

move=> /orP[|] /andP[]; [exact: pdadde_eq0|exact: ndadde_eq0]. Qed.

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

Proof.

rewrite dual_sumeE eqe_oppLRP /= esum_eqNyP.
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP.
Qed.

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

Proof.

rewrite dual_sumeE eqe_oppLR esum_eqNy.
by under eq_existsb => i do rewrite eqe_oppLR.
Qed.

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

Proof.

move=> fioo.
rewrite dual_sumeE eqe_oppLRP /= esum_eqyP => [i Pi|].
by rewrite eqe_oppLR fioo.
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP.
Qed.

Lemma ( : finType) ( : I -> \bar^d R) ( : {pred I}) :
(forall , f i != +oo) ->
(\sum_( | P i) f i == -oo) = [exists in P, f i == -oo].

Proof.

move=> finoo.
rewrite dual_sumeE eqe_oppLR /= esum_eqy => [i|]; rewrite ?eqe_oppLR //.
by under eq_existsb => i do rewrite eqe_oppLR.
Qed.

Lemma : 0 <= x -> 0 <= y -> 0 <= x + y.

Proof.

rewrite dual_addeE oppe_ge0 -!oppe_le0; exact: adde_le0. Qed.

Lemma : x <= 0 -> y <= 0 -> x + y <= 0.

Proof.

rewrite dual_addeE oppe_le0 -!oppe_ge0; exact: adde_ge0. Qed.

Lemma ( : T -> \bar^d R) ( : pred T) :
(forall , P n -> 0 <= f n) -> forall , 0 <= \sum_( <- l | P i) f i.

Proof.

move=> u0 l; rewrite dual_sumeE oppe_ge0 sume_le0 // => t Pt.
rewrite oppe_le0; exact: u0.
Qed.

Lemma ( : T -> \bar^d R) ( : pred T) :
(forall , P n -> f n <= 0) -> forall , \sum_( <- l | P i) f i <= 0.

Proof.

move=> u0 l; rewrite dual_sumeE oppe_le0 sume_ge0 // => t Pt.
rewrite oppe_ge0; exact: u0.
Qed.

Lemma ( : \bar^d R) : (0 < r)%E -> (- r < r)%E.

Proof.

by case: r => //= r; rewrite !lte_fin; apply: gtrN. Qed.

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

Proof.

by elim: n => //= n ->. Qed.

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

Proof.

by elim: n => //= n ->. Qed.

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

Proof.

by elim: n => //= n <-. Qed.

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

Proof.

case: x => [x| |]; case: n => [//|n].
- by rewrite -EFin_natmul -EFin_dnatmul.
- by rewrite enatmul_pinfty ednatmul_pinfty.
- by rewrite enatmul_ninfty ednatmul_ninfty.
Qed.

Lemma : x *+ 2 = x + x

Proof.

by []. Qed.

Lemma : x + y \is a fin_num ->
(x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2.

Proof.

case: x y => [x||] [y||] // _.
by rewrite -EFinM -EFin_dnatmul -!EFin_expe -!dEFinD sqrrD.
Qed.

End DualERealArithTh_numDomainType.

End DualAddTheoryNumDomain.

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

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

Proof.

by rewrite fin_numE -leye_eq -leeNy_eq -2!ltNge. Qed.

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

Proof.

by rewrite fin_numElt; exact: idP. Qed.

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

Proof.

by case: x => // x //=; exact: ltry. Qed.

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

Proof.

by case: x => // x //=; exact: ltNyr. Qed.

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

Proof.

by move: x => [x| |] => // x0; rewrite fin_numElt ltNyr. Qed.

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

Proof.

by move/ltW; exact: ge0_fin_numE. Qed.

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

Proof.

by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed.

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

Proof.

by move/ltW; exact: le0_fin_numE. Qed.

Lemma : a < x < b -> x \is a fin_num.

Proof.

rewrite fin_numE -ltey -ltNye.
by move=> /andP[/(le_lt_trans (leNye _))->/=] /lt_le_trans -> //; exact: leey.
Qed.

Lemma : x = +oo <-> (forall , (0 < A)%R -> A%:E <= x).

Proof.

split=> [-> // A A0|Ax]; first by rewrite leey.
apply/eqP; rewrite eq_le leey /= leNgt; apply/negP.
case: x Ax => [x Ax _|//|/(_ _ ltr01)//].
suff: ~ x%:E < (Order.max 0 x + 1)%:E.
by apply; rewrite lte_fin ltr_pwDr// le_max lexx orbT.
by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_max lexx.
Qed.

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

Proof.

move=> F0; apply/eqP/allP => PF0; last first.
  rewrite big_seq_cond big1// => i /andP[ir Pi].
  by have := PF0 _ ir; rewrite Pi implyTb => /eqP.
move=> i ir; apply/implyP => Pi; apply/eqP.
have rPF : {in r, forall , P i ==> (F i \is a fin_num)}.
  move=> j jr; apply/implyP => Pj; rewrite fin_numElt; apply/andP; split.
    by rewrite (lt_le_trans _ (F0 _ Pj))// ltNyr.
  rewrite ltNge; apply/eqP; rewrite leye_eq; apply/eqP/negP => /eqP Fjoo.
  have PFninfty k : P k -> F k != -oo%E.
    by move=> Pk; rewrite gt_eqF// (lt_le_trans _ (F0 _ Pk))// ltNyr.
  have /esum_eqyP : exists , [/\ i \in r, P i & F i = +oo%E] by exists j.
  by move=> /(_ PFninfty); rewrite PF0.
have ? : (\sum_( <- r | P i) (fine \o F) i == 0)%R.
  apply/eqP/EFin_inj; rewrite big_seq_cond -sumEFin.
  rewrite (eq_bigr (fun => F i0)).
    move=> j /andP[jr Pj] /=; rewrite fineK//.
    by have := rPF _ jr; rewrite Pj implyTb.
  by rewrite -big_seq_cond PF0.
have /allP/(_ _ ir) : all (fun => P i ==> ((fine \o F) i == 0))%R r.
  by rewrite -psumr_eq0// => j Pj/=; apply/fine_ge0/F0.
rewrite Pi implyTb => /= => /eqP Fi0.
rewrite -(@fineK _ (F i))//; first by have := rPF _ ir; rewrite Pi implyTb.
by rewrite Fi0.
Qed.

Lemma : x < +oo -> y < +oo -> x + y < +oo.

Proof.

by move: x y => -[r [r'| |]| |] // ? ?; rewrite -EFinD ltry. Qed.

Lemma : x + y < 0 -> (x < 0) || (y < 0).

Proof.

move: x y => [x| |] [y| |]//; rewrite ?lee_fin ?lte_fin.
- rewrite !ltNge -negb_and; apply: contra.
by move=> /andP[? ?]; rewrite addr_ge0.
- by move=> _; rewrite ltNyr orbT.
- by move=> _; rewrite ltNyr.
- by move=> _; rewrite ltNy0.
- by rewrite ltNy0.
Qed.

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

Proof.

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

Proof.

by move: x y => [r | |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin subr_gt0.
Qed.

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

Proof.

by rewrite !leNgt sube_gt0. Qed.

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

Proof.

by move: x y => [x| |] [y| |] //= _; rewrite ?(leey, lee_fin, subr_ge0).
Qed.

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

Proof.

by move: x y => [x| |] [y| |] //=; rewrite ?(leey, leNye, lee_fin) //= subr_ge0.
Qed.

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

Proof.

by move=> /orP[?|?]; [rewrite suber_ge0|rewrite subre_ge0]. Qed.

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

Proof.

by move: x y => [r| |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin ltrNl.
Qed.

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

Proof.

by move: x y => [r| |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin ltrNr.
Qed.

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

Proof.

by move: x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin lerNr.
Qed.

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

Proof.

by move: x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin lerNl.
Qed.

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

Proof.

by rewrite real_muleN ?real_fine ?num_real. Qed.

Lemma : - x * y = - (x * y)

Proof.

by rewrite muleC muleN muleC. Qed.

Lemma : - x * - y = x * y

Proof.

by rewrite mulNe muleN oppeK. Qed.

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

Proof.

by rewrite [LHS]real_mulry// num_real. Qed.

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

Proof.

by rewrite muleC mulry. Qed.

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

Proof.

by rewrite [LHS]real_mulrNy// num_real. Qed.

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

Proof.

by rewrite muleC mulrNy. Qed.

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

Lemma : 0 <= x -> x \is a fin_num -> y < +oo -> x * y < +oo.

Proof.

move: x y => [x| |] [y| |] // x0 xfin _; first by rewrite -EFinM ltry.
rewrite mulr_infty; move: x0; rewrite lee_fin le_eqVlt => /predU1P[<-|x0].
- by rewrite sgr0 mul0e ltry.
- by rewrite gtr0_sg // mul1e.
Qed.

Lemma : 0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y).

Proof.

move: x y => [x| |] [y| |] //; rewrite ?lee_fin.
- by move=> x0 y0; rewrite !lte_fin; exact: mulr_ge0_gt0.
- rewrite le_eqVlt => /predU1P[<-|x0] _; first by rewrite mul0e ltxx.
  by rewrite ltry andbT mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- move=> _; rewrite le_eqVlt => /predU1P[<-|x0].
    by rewrite mule0 ltxx andbC.
  by rewrite ltry/= mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- by move=> _ _; rewrite mulyy ltry.
Qed.

Lemma : (0 < x -> +oo * x = +oo)%E.

Proof.

move: x => [x|_|//]; last by rewrite mulyy.
by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e.
Qed.

Lemma : (x < 0 -> +oo * x = -oo)%E.

Proof.

move: x => [x|//|_]; last by rewrite mulyNy.
by rewrite lte_fin => x0; rewrite muleC mulr_infty ltr0_sg// mulN1e.
Qed.

Lemma : (0 < x -> -oo * x = -oo)%E.

Proof.

move: x => [x|_|//]; last by rewrite mulNyy.
by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e.
Qed.

Lemma : (x < 0 -> -oo * x = +oo)%E.

Proof.

move: x => [x|//|_]; last by rewrite mulNyNy.
by rewrite lte_fin => x0; rewrite muleC mulr_infty ltr0_sg// mulN1e.
Qed.

Lemma : (0 < x -> x * +oo = +oo)%E.

Proof.

by move=> /gt0_mulye; rewrite muleC; apply. Qed.

Lemma : (x < 0 -> x * +oo = -oo)%E.

Proof.

by move=> /lt0_mulye; rewrite muleC; apply. Qed.

Lemma : (0 < x -> x * -oo = -oo)%E.

Proof.

by move=> /gt0_mulNye; rewrite muleC; apply. Qed.

Lemma : (x < 0 -> x * -oo = +oo)%E.

Proof.

by move=> /lt0_mulNye; rewrite muleC; apply. Qed.

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

Proof.

move: x y => [x| |] [y| |]; rewrite ?(lte_fin,andbF,andbT,orbF,eqxx,andbT)//=.
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite ltry.
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite ltNyr.
Qed.

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

Proof.

have := mule_eq_pinfty x (- y); rewrite muleN eqe_oppLR => ->.
by rewrite !eqe_oppLR lteNr lteNl oppe0 (orbC _ ((x == -oo) && _)).
Qed.

Lemma : a < b -> x < y -> a + x < b + y.

Proof.

move: a b x y=> [a| |] [b| |] [x| |] [y| |]; rewrite ?(ltry,ltNyr)//.
by rewrite !lte_fin; exact: ltrD.
Qed.

Lemma : 0 <= y -> x <= x + y.

Proof.

move: x y => -[ x [y| |]//= | [| |]// | [| | ]//];
by [rewrite !lee_fin lerDl | move=> _; exact: leey].
Qed.

Lemma : 0 <= y -> x <= y + x.

Proof.

by rewrite addeC; exact: leeDl. Qed.

Lemma : y <= 0 -> x + y <= x.

Proof.

move: x y => -[ x [y| |]//= | [| |]// | [| | ]//];
by [rewrite !lee_fin gerDl | move=> _; exact: leNye].
Qed.

Lemma : y <= 0 -> y + x <= x

Proof.

rewrite addeC; exact: geeDl. Qed.

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

Proof.

by move: x y => [x| |] [y| |] _ //; rewrite ?ltry ?ltNyr // !lte_fin ltrDl.
Qed.

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

Proof.

rewrite addeC; exact: lteDl. Qed.

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

Proof.

move: y x => [x| |] [y| |] _ //; rewrite addeC /= ?ltNyr ?ltry//.
by rewrite !lte_fin gtrDr ltrNl oppr0.
Qed.

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

Proof.

by rewrite addeC; exact: gte_subl. Qed.

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

Proof.

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

Proof.

by rewrite addeC; exact: gteDl. Qed.

Lemma : x \is a fin_num -> (x + a < x + b) = (a < b).

Proof.

move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(ltry, ltNyr)//.
by rewrite !lte_fin ltrD2l.
Qed.

Lemma : x \is a fin_num -> (a + x < b + x) = (a < b).

Proof.

by rewrite -!(addeC x); exact: lteD2lE. Qed.

Lemma : a <= b -> x + a <= x + b.

Proof.

move: a b x => -[a [b [x /=|//|//] | []// |//] | []// | ].
- by rewrite !lee_fin lerD2l.
- by move=> r _; exact: leey.
- by move=> -[b [| |]// | []// | //] r oob; exact: leNye.
Qed.

Lemma : x \is a fin_num -> (x + a <= x + b) = (a <= b).

Proof.

move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(leey, leNye)//.
by rewrite !lee_fin lerD2l.
Qed.

Lemma : x \is a fin_num -> (a + x <= b + x) = (a <= b).

Proof.

by rewrite -!(addeC x); exact: leeD2lE. Qed.

Lemma : a <= b -> a + x <= b + x.

Proof.

rewrite addeC (addeC b); exact: leeD2l. Qed.

Lemma : a <= b -> x <= y -> a + x <= b + y.

Proof.

move: a b x y => [a| |] [b| |] [x| |] [y| |]; rewrite ?(leey, leNye)//.
by rewrite !lee_fin; exact: lerD.
Qed.

Lemma : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.

Proof.

move: x y a b => [x| |] [y| |] [a| |] [b| |] _ //=; rewrite ?(ltry, ltNyr)//.
by rewrite !lte_fin; exact: ltr_leD.
Qed.

Lemma : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.

Proof.

by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_leD. Qed.

Lemma : x <= y -> u <= z -> x - z <= y - u.

Proof.

move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//.
by rewrite !lee_fin; exact: lerB.
Qed.

Lemma : u \is a fin_num ->
x < z -> u <= y -> x - y < z - u.

Proof.

move: z u x y => [z| |] [u| |] [x| |] [y| |] _ //=; rewrite ?(ltry, ltNyr)//.
by rewrite !lte_fin => xltr tley; apply: ltr_leD; rewrite // lerNl opprK.
Qed.

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

Proof.

move: z => [z| |] _ // z0 [x| |] [y| |] //.
- by rewrite !lte_fin ltr_pM2r.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty gtr0_sg// mul1e ltNge leNye ltNge leNye.
- by rewrite mulr_infty gtr0_sg// mul1e ltNge leey ltNge leey.
- by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltNyr.
- by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
Qed.

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

Proof.

by move=> zfin z0 x y; rewrite 2!(muleC z) lte_pmul2r. Qed.

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

Proof.

rewrite -oppe0 lteNr => zfin z0 x y.
by rewrite -(oppeK z) !mulNe lteNl oppeK -2!mulNe lte_pmul2l ?fin_numN.
Qed.

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

Proof.

by move=> zfin z0 x y; rewrite -!(muleC z) lte_nmul2l. Qed.

Lemma : y \is a fin_num -> 0 < y -> (y < y * x) = (1 < x).

Proof.

by move=> yfin y0; rewrite -[X in (X < _) = _]mule1 lte_pmul2l. Qed.

Lemma : y \is a fin_num -> 0 < y -> (y < x * y) = (1 < x).

Proof.

by move=> yfin y0; rewrite muleC lte_pmulr. Qed.

Lemma : y \is a fin_num -> y < 0 -> (y < y * x) = (x < 1).

Proof.

by move=> yfin y0; rewrite -[X in (X < _) = _]mule1 lte_nmul2l. Qed.

Lemma : y \is a fin_num -> y < 0 -> (y < x * y) = (x < 1).

Proof.

by move=> yfin y0; rewrite muleC lte_nmulr. Qed.

Lemma ( : I -> \bar R) ( : pred I) :
(forall , P i -> f i <= g i) ->
\sum_( <- s | P i) f i <= \sum_( <- s | P i) g i.

Proof.

by move=> Pfg; elim/big_ind2 : _ => // *; exact: leeD. Qed.

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

Proof.

move=> QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i.
by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP.
Qed.

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

Proof.

move=> QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i.
by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP.
Qed.

Lemma ( : eqType) ( : seq I) ( : pred I)
( : I -> \bar R) : (forall , P i -> ~~ Q i -> 0 <= f i) ->
\sum_( <- s | P i && Q i) f i <= \sum_( <- s | P i) f i.

Proof.

move=> PQf; rewrite [leRHS](bigID Q) /= -[leLHS]adde0 leeD //.
by rewrite sume_ge0// => i /andP[]; exact: PQf.
Qed.

Lemma ( : eqType) ( : seq I) ( : pred I)
( : I -> \bar R) : (forall , P i -> ~~ Q i -> f i <= 0) ->
\sum_( <- s | P i) f i <= \sum_( <- s | P i && Q i) f i.

Proof.

move=> PQf; rewrite [leLHS](bigID Q) /= -[leRHS]adde0 leeD //.
by rewrite sume_le0// => i /andP[]; exact: PQf.
Qed.

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

Proof.

move=> f0 i j le_ij; rewrite (big_ord_widen_cond j) // big_mkcondr /=.
by rewrite lee_sum // => k ?; case: ifP => // _; exact: f0.
Qed.

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

Proof.

move=> f0 m n ?; rewrite [leRHS](big_ord_widen_cond n) // big_mkcondr /=.
by rewrite lee_sum // => i ?; case: ifP => // _; exact: f0.
Qed.

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

Proof.

move=> f0 i j le_ij; rewrite -[m]add0n !big_addn !big_mkord.
apply: (@lee_sum_nneg_ord (fun => f (k + m)%N) (fun => P (k + m)%N));
by [move=> n /f0; apply; rewrite leq_addl | rewrite leq_sub2r].
Qed.

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

Proof.

move=> f0 i j le_ij; rewrite -[m]add0n !big_addn !big_mkord.
apply: (@lee_sum_npos_ord (fun => f (k + m)%N) (fun => P (k + m)%N));
by [move=> n /f0; apply; rewrite leq_addl | rewrite leq_sub2r].
Qed.

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

Proof.

move=> f0 i j le_ij; rewrite !big_geq_mkord/=.
rewrite lee_sum_nneg_subset// => [k | k /and3P[_ /f0->//]].
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->].
Qed.

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

Proof.

move=> f0 i j le_ij; rewrite !big_geq_mkord/=.
rewrite lee_sum_npos_subset// => [k | k /and3P[_ /f0->//]].
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->].
Qed.

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

Proof.

move=> AB f0; rewrite [leRHS]big_mkcond (big_fsetID _ (mem A) B) /=.
rewrite -[leLHS]adde0 leeD //.
rewrite -big_mkcond /= {1}(_ : A = [fset in B | x \in A]%fset) //.
by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_ge0 // => t /andP[tB tA].
by case: ifPn => // Pt; rewrite f0 // !inE tA.
Qed.

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

Proof.

move=> AB f0; rewrite big_mkcond (big_fsetID _ (mem A) B) /=.
rewrite -[leRHS]adde0 leeD //.
rewrite -big_mkcond /= {3}(_ : A = [fset in B | x \in A]%fset) //.
by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_le0 // => t /andP[tB tA].
by case: ifPn => // Pt; rewrite f0 // !inE tA.
Qed.

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

Proof.

move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltry ?ltNyr //.
by rewrite !lte_fin ltrBlDr.
Qed.

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

Proof.

by move=> ?; rewrite lteBlDr// addeC. Qed.

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

Proof.

move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltNyr ?ltry //.
by rewrite !lte_fin ltrBrDr.
Qed.

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

Proof.

by move=> ?; rewrite lteBrDr// addeC. Qed.

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

Proof.

move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltNyr ?ltry //.
by rewrite !lte_fin ltrBlDr.
Qed.

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

Proof.

by move=> ?; rewrite lte_subel_addr// addeC. Qed.

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

Proof.

move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltNyr ?ltry //.
by rewrite !lte_fin ltrBrDr.
Qed.

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

Proof.

by move=> ?; rewrite lte_suber_addr// addeC. Qed.

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

Proof.

move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?leey ?leNye //.
by rewrite !lee_fin lerBlDr.
Qed.

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

Proof.

by move=> ?; rewrite leeBlDr// addeC. Qed.

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

Proof.

move: y x z => [y| |] [x| |] [z| |] _ //=; rewrite ?leNye ?leey //.
by rewrite !lee_fin lerBrDr.
Qed.

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

Proof.

by move=> ?; rewrite leeBrDr// addeC. Qed.

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

Proof.

move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?leey ?leNye //.
by rewrite !lee_fin lerBlDr.
Qed.

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

Proof.

by move=> ?; rewrite lee_subel_addr// addeC. Qed.

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

Proof.

move: y x z => [y| |] [x| |] [z| |] _ //=; rewrite ?leNye ?leey //.
by rewrite !lee_fin lerBrDr.
Qed.

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

Proof.

by move=> ?; rewrite lee_suber_addr// addeC. Qed.

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

Proof.

by move=> ?; rewrite lte_subel_addr// add0e. Qed.

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

Proof.

by move=> ?; rewrite lteBlDl// adde0. Qed.

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

Proof.

by move=> /orP[?|?]; [rewrite subre_lt0|rewrite suber_lt0]. Qed.

Lemma : 0 < x -> (x * y >= 0) = (y >= 0).

Proof.

move=> x_gt0; apply/idP/idP; last exact/mule_ge0/ltW.
by apply: contra_le; apply: mule_gt0_lt0.
Qed.

Lemma : 0 < x -> (y * x >= 0) = (y >= 0).

Proof.

by rewrite muleC; apply: pmule_rge0. Qed.

Lemma : 0 < x -> (x * y < 0) = (y < 0).

Proof.

by move=> /pmule_rge0; rewrite !ltNge => ->. Qed.

Lemma : 0 < x -> (y * x < 0) = (y < 0).

Proof.

by rewrite muleC; apply: pmule_rlt0. Qed.

Lemma : 0 < x -> (x * y <= 0) = (y <= 0).

Proof.

by move=> xgt0; rewrite -oppe_ge0 -muleN pmule_rge0 ?oppe_ge0. Qed.

Lemma : 0 < x -> (y * x <= 0) = (y <= 0).

Proof.

by rewrite muleC; apply: pmule_rle0. Qed.

Lemma : 0 < x -> (x * y > 0) = (y > 0).

Proof.

by move=> xgt0; rewrite -oppe_lt0 -muleN pmule_rlt0 ?oppe_lt0. Qed.

Lemma : 0 < x -> (y * x > 0) = (y > 0).

Proof.

by rewrite muleC; apply: pmule_rgt0. Qed.

Lemma : x < 0 -> (x * y >= 0) = (y <= 0).

Proof.

by rewrite -oppe_gt0 => /pmule_rle0<-; rewrite mulNe oppe_le0. Qed.

Lemma : x < 0 -> (y * x >= 0) = (y <= 0).

Proof.

by rewrite muleC; apply: nmule_rge0. Qed.

Lemma : x < 0 -> (x * y <= 0) = (y >= 0).

Proof.

by rewrite -oppe_gt0 => /pmule_rge0<-; rewrite mulNe oppe_ge0. Qed.

Lemma : x < 0 -> (y * x <= 0) = (y >= 0).

Proof.

by rewrite muleC; apply: nmule_rle0. Qed.

Lemma : x < 0 -> (x * y > 0) = (y < 0).

Proof.

by rewrite -oppe_gt0 => /pmule_rlt0<-; rewrite mulNe oppe_lt0. Qed.

Lemma : x < 0 -> (y * x > 0) = (y < 0).

Proof.

by rewrite muleC; apply: nmule_rgt0. Qed.

Lemma : x < 0 -> (x * y < 0) = (y > 0).

Proof.

by rewrite -oppe_gt0 => /pmule_rgt0<-; rewrite mulNe oppe_gt0. Qed.

Lemma : x < 0 -> (y * x < 0) = (y > 0).

Proof.

by rewrite muleC; apply: nmule_rlt0. Qed.

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

Proof.

have [xlt0|xgt0|->] := ltgtP x 0; last by rewrite mul0e.
by rewrite nmule_rlt0//= -leNgt lt_def.
by rewrite pmule_rlt0//= !lt_neqAle andbA andbb.
Qed.

Lemma : associative ( *%E : \bar R -> \bar R -> \bar R ).

Proof.

move=> x y z.
wlog x0 : x y z / 0 < x => [hwlog|].
  have [x0| |->] := ltgtP x 0; [ |exact: hwlog|by rewrite !mul0e].
  by apply: oppe_inj; rewrite -!mulNe hwlog ?oppe_gt0.
wlog y0 : x y z x0 / 0 < y => [hwlog|].
  have [y0| |->] := ltgtP y 0; [ |exact: hwlog|by rewrite !(mul0e, mule0)].
  by apply: oppe_inj; rewrite -muleN -2!mulNe -muleN hwlog ?oppe_gt0.
wlog z0 : x y z x0 y0 / 0 < z => [hwlog|].
  have [z0| |->] := ltgtP z 0; [ |exact: hwlog|by rewrite !mule0].
  by apply: oppe_inj; rewrite -!muleN hwlog ?oppe_gt0.
case: x x0 => [x x0| |//]; last by rewrite !gt0_mulye ?mule_gt0.
case: y y0 => [y y0| |//]; last by rewrite gt0_mulye // muleC !gt0_mulye.
case: z z0 => [z z0| |//]; last by rewrite !gt0_muley ?mule_gt0.
by rewrite /mule/= mulrA.
Qed.

Lemma : iter n ( *%E x) y = x ^+ n * y.

Proof.

by elim: n => [|n ih]; rewrite ?mul1e// [LHS]/= ih expeS muleA. Qed.

..isComLaw.Build (\bar R) 1 mule
muleA muleC mul1e.

Lemma : left_commutative ( *%E : \bar R -> \bar R -> \bar R ).

Proof.

exact: Monoid.mulmCA. Qed.

Lemma : right_commutative ( *%E : \bar R -> \bar R -> \bar R ).

Proof.

exact: Monoid.mulmAC. Qed.

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

Proof.

exact: Monoid.mulmACA. Qed.

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

Proof.

rewrite /mule/=; move: x y z => [x| |] [y| |] [z| |] //= _; try
(by case: ltgtP => // -[] <-; rewrite ?(mul0r,add0r,adde0))
|| (by case: ltgtP => //; rewrite adde0).
by rewrite mulrDr.
Qed.

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

Proof.

by move=> ? ?; rewrite -!(muleC x) muleDr. Qed.

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

Proof.

by move=> ? yz; rewrite muleDr ?muleN. Qed.

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

Proof.

by move=> ? yz; rewrite muleDl// mulNe. Qed.

Lemma : 0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x.

Proof.

rewrite /mule/=; move: x y z => [r| |] [s| |] [t| |] //= s0 t0.
- by rewrite mulrDl.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => //; rewrite adde0.
- rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin.
  case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
  + rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0.
    by case: ltgtP t0 => // [t0|[<-{t}]] _; [rewrite gt_eqF|rewrite eqxx].
  + by move: t0; rewrite lee_fin; case: (ltgtP t).
- by case: ltgtP s0.
- by case: ltgtP t0.
- rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin.
  case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
  + rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0.
    by case: ltgtP t0 => // [t0|[<-{t}]].
  + by move: t0; rewrite lee_fin; case: (ltgtP t).
- by case: ltgtP s0.
Qed.

Lemma : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z.

Proof.

by move=> y0 z0; rewrite !(muleC x) ge0_muleDl. Qed.

Lemma : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x.

Proof.

rewrite /mule/=; move: x y z => [r| |] [s| |] [t| |] //= s0 t0.
- by rewrite mulrDl.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => //; rewrite adde0.
- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin.
  case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
  + rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=.
    by rewrite !ltNge ltW //.
  + by case: (ltgtP t).
- by case: ltgtP s0.
- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin.
  case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
  + rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=.
    by rewrite !ltNge ltW // -lee_fin t0; case: eqP.
  + by case: (ltgtP t).
- by rewrite ltNge s0 /=; case: eqP.
- by rewrite ltNge t0 /=; case: eqP.
Qed.

Lemma : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z.

Proof.

by move=> y0 z0; rewrite !(muleC x) le0_muleDl. Qed.

Lemma : r%:E^-1 = if r == 0%R then +oo else r^-1%R%:E.

Proof.

by []. Qed.

Variant : \bar R -> \bar R -> Type :=
| : inve_spec 0 +oo
| : inve_spec +oo 0
| : inve_spec -oo -oo
| : r != 0%R -> inve_spec r%:E r^-1%:E.

Lemma : inve_spec x x^-1.

Proof.

rewrite /inve; case: x => [r||]/=; do ?by constructor.
by case: eqVneq => // [->|]; constructor.
Qed.

Lemma : fine r%:E^-1 = r^-1%R.

Proof.

by rewrite inver; case: eqP => //= ->; rewrite invr0. Qed.

Lemma : 0^-1 = +oo :> \bar R

Proof.

by rewrite inver eqxx. Qed.

Lemma : 1^-1 = 1 :> \bar R

Proof.

by rewrite inver oner_eq0 invr1. Qed.

Lemma : +oo^-1 = 0 :> \bar R

Proof.

by []. Qed.

Lemma : -oo^-1 = -oo :> \bar R

Proof.

by []. Qed.

Lemma : involutive (inve : \bar R -> \bar R).

Proof.

move=> x; case: (inveP x); rewrite ?inve0//= => r r_neq0.
by rewrite inver invr_eq0 (negPf r_neq0) invrK.
Qed.

Lemma : injective (inve : \bar R -> \bar R).

Proof.

exact: can_inj inveK. Qed.

Lemma : x \is a fin_num -> x != 0 -> (- x)^-1 = - x^-1.

Proof.

case: (inveP x); rewrite ?eqxx//= => r r_neq0 _ _; rewrite EFinN.
by rewrite -invrN// inver oppr_eq0 (negPf r_neq0).
Qed.

Lemma : (x^-1 == 0) = (x == +oo).

Proof.

by case: inveP; rewrite ?eqxx //= => r /negPf; rewrite eqe invr_eq0. Qed.

Lemma : (x^-1 == 1) = (x == 1).

Proof.

move: x => [x| |]/=.
- rewrite inver; case: ifPn => [/eqP ->|x0]; last by rewrite !eqe invr_eq1.
by rewrite eqe// [RHS]eq_sym oner_eq0; apply/negbTE.
- by rewrite invey eq_sym onee_eq0.
- by rewrite inveNy.
Qed.

Lemma : (x^-1 == +oo) = (x == 0).

Proof.

case: x => [r| |] //=; apply/idP/idP => [|]; first by rewrite inver; case: ifPn.
by rewrite eqe => /eqP ->; rewrite inver// eqxx.
Qed.

Lemma : (x^-1 == -oo) = (x == -oo).

Proof.

by case: x => [r| |] //=; rewrite inver; case: ifPn. Qed.

Lemma : (0 <= x^-1) = (0 <= x).

Proof.

by case: inveP; rewrite ?le0y ?lexx //= => r; rewrite lee_fin invr_ge0.
Qed.

Lemma : x != 0 -> x != +oo -> (0 < x^-1) = (0 < x).

Proof.

rewrite !lt_def inve_eq0 inve_ge0.
by case: leP => /[!(andbT, andbF)]//= _ -> ->.
Qed.

Lemma : reflect ((0 < x^-1) = (0 < x)) ((x != 0) && (x != +oo)).

Proof.

apply/(iffP idP); first by move=> /andP[]; exact:inve_gt0.
case: eqP => [->|x0]; first by rewrite inve0 lt0y ltxx.
by case: eqP => [->|xy]; first by rewrite invey ltxx lt0y.
Qed.

Lemma : reflect ((x^-1 <= 0) = (x <= 0)) ((x != 0) && (x != +oo)).

Proof.

by rewrite !leNgt; apply/(iffP idP)=> [/inve_gt0P->|/negb_inj /inve_gt0P].
Qed.

Lemma : x != 0 -> x != +oo -> (x^-1 <= 0) = (x <= 0).

Proof.

by move=> xN0 xNy; rewrite !leNgt inve_gt0. Qed.

Lemma : (x^-1 < 0) = (x < 0).

Proof.

by rewrite !ltNge inve_ge0. Qed.

Lemma : x != 0 -> x != -oo -> x^-1 \is a fin_num.

Proof.

by move: x => [x| |]//; rewrite eqe => x0 _; rewrite inver (negbTE x0).
Qed.

Lemma : 1 / x = x^-1.

Proof.

move: x => [x| |]/=; first by rewrite mul1e.
- by rewrite invey mule0.
- by rewrite inveNy mul1e.
Qed.

Lemma : y \is a fin_num -> 0 <= x -> y <= 1 -> y * x <= x.

Proof.

move=> yfin; rewrite le_eqVlt => /predU1P[<-|]; first by rewrite mule0.
move: x y yfin => [x| |] [y| |] //= _.
- by rewrite lte_fin => x0 y1; rewrite lee_fin ger_pMl.
- by move=> _; rewrite /mule/= eqe => r1; rewrite leey.
Qed.

Lemma : 0 <= x -> {homo *%E^~ x : / y <= z}.

Proof.

move: x => [x|_|//].
  rewrite lee_fin le_eqVlt => /predU1P[<- y z|x0]; first by rewrite 2!mule0.
  move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r.
  - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey.
  - by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye.
  - by move=> _; rewrite mulNyr mulyr gtr0_sg// 2!mul1e.
move=> [y| |] [z| |]//.
- rewrite lee_fin => yz.
  have [z0|z0|] := ltgtP 0%R z.
  + by rewrite [leRHS]mulr_infty gtr0_sg// mul1e leey.
  + by rewrite mulr_infty ltr0_sg// ?(le_lt_trans yz)// [leRHS]mulr_infty ltr0_sg.
  + move=> z0; move: yz; rewrite -z0 mul0e le_eqVlt => /predU1P[->|y0].
      by rewrite mul0e.
    by rewrite mulr_infty ltr0_sg// mulN1e leNye.
  + by move=> _; rewrite mulyy leey.
  + by move=> _; rewrite mulNyy leNye.
Qed.

Lemma : 0 <= x -> {homo *%E x : / y <= z}.

Proof.

by move=> x0 y z yz; rewrite !(muleC x) lee_wpmul2r. Qed.

Lemma ( : Type) ( : seq I) ( : pred I) ( : I -> \bar R) :
(forall , P i -> 0 <= F i) ->
(\sum_( <- s | P i) F i) * x = \sum_( <- s | P i) (F i * x).

Proof.

elim: s x P F => [x P F F0|h t ih x P F F0]; first by rewrite 2!big_nil mul0e.
rewrite big_cons; case: ifPn => Ph; last by rewrite big_cons (negbTE Ph) ih.
by rewrite ge0_muleDl ?sume_ge0// ?F0// ih// big_cons Ph.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I) ( : I -> \bar R) :
(forall , P i -> 0 <= F i) ->
x * (\sum_( <- s | P i) F i) = \sum_( <- s | P i) (x * F i).

Proof.

by move=> F0; rewrite muleC ge0_sume_distrl//; under eq_bigr do rewrite muleC.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I) ( : I -> \bar R) :
(forall , P i -> F i <= 0) ->
(\sum_( <- s | P i) F i) * x = \sum_( <- s | P i) (F i * x).

Proof.

elim: s x P F => [x P F F0|h t ih x P F F0]; first by rewrite 2!big_nil mul0e.
rewrite big_cons; case: ifPn => Ph; last by rewrite big_cons (negbTE Ph) ih.
by rewrite le0_muleDl ?sume_le0// ?F0// ih// big_cons Ph.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I) ( : I -> \bar R) :
(forall , P i -> F i <= 0) ->
x * (\sum_( <- s | P i) F i) = \sum_( <- s | P i) (x * F i).

Proof.

by move=> F0; rewrite muleC le0_sume_distrl//; under eq_bigr do rewrite muleC.
Qed.

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

Proof.

move=> xfin PF; elim: s => [|h t ih]; first by rewrite !big_nil mule0.
rewrite !big_cons; case: ifPn => Ph //.
by rewrite muleDr// ?ih// adde_def_sum// => i Pi; rewrite PF.
Qed.

Lemma : (forall , r%:E <= x) -> x = +oo.

Proof.

case: x => [x /(_ (x + 1)%R)|//|/(_ 0%R)//].
by rewrite EFinD addeC -leeBrDr// subee// lee_fin ler10.
Qed.

Lemma : (forall , x <= r%:E) -> x = -oo.

Proof.

move=> *; apply: (can_inj oppeK); apply: eq_infty => r.
by rewrite leeNr -EFinN.
Qed.

Lemma : x <= `|x|.

Proof.

by move: x => [x| |]//=; rewrite lee_fin ler_norm. Qed.

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

Proof.

by move: x => [x| |] //=; rewrite normr_id. Qed.

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

Proof.

by move: x y => [x| |] [y| |] //=; rewrite ?lte_fin ?ltry ?ltNyr// ltr_norml.
Qed.

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

Proof.

by move: x y => [x| |] [y| |] //=; rewrite? leey// !eqe eqr_norml lee_fin.
Qed.

Lemma : `|x + y| <= `|x| + `|y|.

Proof.

by move: x y => [x| |] [y| |] //; rewrite /abse -EFinD lee_fin ler_normD.
Qed.

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

Proof.

elim/big_ind2 : _ => //; first by rewrite abse0.
by move=> *; exact/(le_trans (lee_abs_add _ _) (leeD _ _)).
Qed.

Lemma : `|x - y| <= `|x| + `|y|.

Proof.

by move: x y => [x| |] [y| |] //; rewrite /abse -EFinD lee_fin ler_normB.
Qed.

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

Proof.

have xoo r : `|r%:E * +oo| = `|r|%:E * +oo.
  have [r0|r0] := leP 0%R r.
    by rewrite (ger0_norm r0)// gee0_abs// mule_ge0// leey.
  rewrite (ltr0_norm r0)// lte0_abs// ?EFinN ?mulNe//.
  by rewrite mule_lt0 /= eqe lt_eqF//= lte_fin r0.
move=> [x| |] [y| |] //=; first by rewrite normrM.
- by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- by rewrite muleC xoo muleC.
- by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
Qed.

Lemma { : Type} ( : seq I) ( : pred I) ( : I -> \bar R) :
`|\prod_( <- r | P i) F i| = \prod_( <- r | P i) `|F i|.

Proof.

elim/big_ind2 : _ => //; first by rewrite abse1.
by move=> ? ? ? ? <- <-; rewrite abseM.
Qed.

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

Proof.

Lemma { : Type} ( : seq I) ( : I -> bool) ( : I -> R) :
\big[maxe/r%:E]_( <- s | P i) (F i)%:E =
(\big[Num.max/r]_( <- s | P i) F i)%:E.

Proof.

by rewrite (big_morph _ EFin_max erefl). Qed.

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

Proof.

Lemma : left_distributive (@GRing.add (\bar R)) maxe.

Proof.

move=> x y z; have [xy|yx] := leP x y.
by apply/esym/max_idPr; rewrite leeD2r.
by apply/esym/max_idPl; rewrite leeD2r// ltW.
Qed.

Lemma : right_distributive (@GRing.add (\bar R)) maxe.

Proof.

move=> x y z; have [yz|zy] := leP y z.
by apply/esym/max_idPr; rewrite leeD2l.
by apply/esym/max_idPl; rewrite leeD2l// ltW.
Qed.

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

Proof.

by move=> x; rewrite maxC maxye. Qed.

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

Proof.

by move=> x; have [//|] := leP -oo x; rewrite ltNge leNye. Qed.

.
Monoid.isLaw.Build (\bar R) -oo maxe maxA maxNye maxeNy.

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

Proof.

by move=> x; have [|//] := leP x -oo; rewrite leeNy_eq => /eqP. Qed.

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

Proof.

by move=> x; rewrite minC minye. Qed.

.
Monoid.isLaw.Build (\bar R) +oo mine minA minye miney.

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

Proof.

move=> [x| |] [y| |] //=.
- by rewrite -fine_max//= -fine_min//= oppr_max.
- by rewrite maxey mineNy.
- by rewrite miney.
- by rewrite minNye.
- by rewrite maxNye minye.
Qed.

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

Proof.

by move=> x y; rewrite -[RHS]oppeK oppe_max !oppeK. Qed.

Lemma : z \is a fin_num -> 0 <= z ->
z * maxe x y = maxe (z * x) (z * y).

Proof.

move=> /[swap]; rewrite le_eqVlt => /predU1P[<- _|z0].
by rewrite !mul0e maxxx.
have [xy|yx|->] := ltgtP x y; last by rewrite maxxx.
- by move=> zfin; rewrite /maxe lte_pmul2l // xy.
- by move=> zfin; rewrite maxC /maxe lte_pmul2l// yx.
Qed.

Lemma : z \is a fin_num -> 0 <= z ->
maxe x y * z = maxe (x * z) (y * z).

Proof.

by move=> zfin z0; rewrite muleC maxe_pMr// !(muleC z). Qed.

Lemma : z \is a fin_num -> 0 <= z ->
z * mine x y = mine (z * x) (z * y).

Proof.

move=> fz zge0.
by rewrite -eqe_oppP -muleN [in LHS]oppe_min maxe_pMr// !muleN -oppe_min.
Qed.

Lemma : z \is a fin_num -> 0 <= z ->
mine x y * z = mine (x * z) (y * z).

Proof.

by move=> zfin z0; rewrite muleC mine_pMr// !(muleC z). Qed.

Lemma ( : seq (\bar R)) : s != [::] ->
{in s, forall , def <= x /\ x \is a fin_num} ->
\big[maxe/def]_( <- s) i \is a fin_num.

Proof.

elim: s => // h [_ _ /(_ h)|h' t ih _ /forall_cons[[defh hfin] h'tfin]].
rewrite mem_seq1 => /(_ (eqxx _))[/max_idPl defh hfin].
by rewrite big_seq1_id defh.
by rewrite big_cons -fine_max// ih.
Qed.

Lemma : 0 <= y -> 1 <= x -> y <= x * y.

Proof.

move: x y => [x| |] [y| |] //.
- by rewrite -EFinM 3!lee_fin; exact: ler_peMl.
- move=> _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e// (lt_le_trans _ x1).
- rewrite lee_fin le_eqVlt => /predU1P[<- _|y0 _]; first by rewrite mule0.
by rewrite mulr_infty gtr0_sg// mul1e leey.
Qed.

Lemma : y <= 0 -> 1 <= x -> x * y <= y.

Proof.

move: x y => [x| |] [y| |] //.
- by rewrite -EFinM 3!lee_fin; exact: ler_neMl.
- move=> _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e// (lt_le_trans _ x1).
- rewrite lee_fin le_eqVlt => /predU1P[-> _|y0 _]; first by rewrite mule0.
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
Qed.

Lemma : 0 <= y -> 1 <= x -> y <= y * x.

Proof.

by move=> y0 x1; rewrite muleC lee_pemull. Qed.

Lemma : y <= 0 -> 1 <= x -> y * x <= y.

Proof.

by move=> y0 x1; rewrite muleC lee_nemull. Qed.

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

Proof.

elim: n => [|n]; first by rewrite mul0e.
move: x => [x| |] ih.
- by rewrite -EFinM mulr_natl EFin_natmul.
- by rewrite mulry gtr0_sg// mul1e enatmul_pinfty.
- by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty.
Qed.

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

Proof.

by rewrite muleC mule_natl. Qed.

Lemma :
0 <= x1 -> 0 <= x2 -> x1 < y1 -> x2 < y2 -> x1 * x2 < y1 * y2.

Proof.

move: x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //;
    rewrite !(lte_fin,lee_fin).
- by move=> *; rewrite ltr_pM.
- move=> x10 x20 xy1 xy2.
  by rewrite mulry gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy1).
- move=> x10 x20 xy1 xy2.
  by rewrite mulyr gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy2).
- by move=> *; rewrite mulyy -EFinM ltry.
Qed.

Lemma : 0 <= x1 -> 0 <= x2 -> x1 <= y1 -> x2 <= y2 ->
x1 * x2 <= y1 * y2.

Proof.

move: x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //; rewrite !lee_fin.
- exact: ler_pM.
- rewrite le_eqVlt => /predU1P[<- x20 y10 _|x10 x20 xy1 _].
    by rewrite mul0e mule_ge0// leey.
  by rewrite mulr_infty gtr0_sg// ?mul1e ?leey// (lt_le_trans x10).
- rewrite le_eqVlt => /predU1P[<- _ y10 _|x10 _ xy1 _].
    by rewrite mul0e mule_ge0// leey.
  rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// ?mul1e//.
  exact: (lt_le_trans x10).
- move=> x10; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].
    by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0.
  by rewrite mulr_infty gtr0_sg ?mul1e ?leey// (lt_le_trans x20).
- by move=> x10 x20 _ _; rewrite mulyy leey.
- rewrite le_eqVlt => /predU1P[<- _ _ _|x10 _ _ _].
    by rewrite mulyy mul0e leey.
  by rewrite mulyy mulr_infty gtr0_sg// mul1e.
- move=> _; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].
    by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0.
  rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg ?mul1e//.
  exact: (lt_le_trans x20).
- move=> _; rewrite le_eqVlt => /predU1P[<- _ _|x20 _ _].
    by rewrite mule0 mulyy leey.
  by rewrite mulr_infty gtr0_sg// mul1e// mulyy.
Qed.

Lemma : x \is a fin_num -> 0 < x -> {mono *%E x : / x <= y}.

Proof.

move: x => [x _|//|//] /[!(@lte_fin R)] x0 [y| |] [z| |].
- by rewrite -2!EFinM 2!lee_fin ler_pM2l.
- by rewrite mulry gtr0_sg// mul1e 2!leey.
- by rewrite mulrNy gtr0_sg// mul1e 2!leeNy_eq.
- by rewrite mulry gtr0_sg// mul1e 2!leye_eq.
- by rewrite mulry gtr0_sg// mul1e.
- by rewrite mulry mulrNy gtr0_sg// mul1e mul1e.
- by rewrite mulrNy gtr0_sg// mul1e 2!leNye.
- by rewrite mulrNy mulry gtr0_sg// 2!mul1e.
- by rewrite mulrNy gtr0_sg// mul1e.
Qed.

Lemma : x \is a fin_num -> 0 < x -> {mono *%E^~ x : / x <= y}.

Proof.

by move=> xfin x0 y z; rewrite -2!(muleC x) lee_pmul2l. Qed.

Lemma : 0 <= x -> 0 <= y -> (x ^+ 2 <= y ^+ 2) = (x <= y).

Proof.

move=> xge0 yge0; apply/idP/idP; rewrite !expe2.
by apply: contra_le => yltx; apply: lte_pmul.
by move=> xley; apply: lee_pmul.
Qed.

Lemma : 0 <= x -> 0 <= y -> (x ^+ 2 < y ^+ 2) = (x < y).

Proof.

move=> xge0 yge0; apply/idP/idP; rewrite !expe2.
by apply: contra_lt => yltx; apply: lee_pmul.
by move=> xley; apply: lte_pmul.
Qed.

Lemma : 0 <= y -> x ^+ 2 <= y ^+ 2 -> x <= y.

Proof.

move=> yge0; have [xge0|xlt0 x2ley2] := leP 0 x; first by rewrite lee_sqr.
exact: le_trans (ltW xlt0) _.
Qed.

Lemma : 0 <= y -> x ^+ 2 < y ^+ 2 -> x < y.

Proof.

move=> yge0; have [xge0|xlt0 x2ley2] := leP 0 x; first by rewrite lte_sqr.
exact: lt_le_trans xlt0 _.
Qed.

Lemma : 0 <= x ^+ 2.

Proof.

by case: x => [x||]; rewrite /= ?mulyy ?mulNyNy ?le0y//; apply: sqr_ge0.
Qed.

Lemma : 0 <= x -> y <= z -> y <= x + z.

Proof.

by move=> *; rewrite -[y]add0e leeD. Qed.

Lemma : 0 <= x -> y < z -> y < x + z.

Proof.

by move=> x0 /lt_le_trans; apply; rewrite lee_paddl. Qed.

Lemma : 0 <= x -> y <= z -> y <= z + x.

Proof.

by move=> *; rewrite addeC lee_paddl. Qed.

Lemma : 0 <= x -> y < z -> y < z + x.

Proof.

by move=> *; rewrite addeC lte_paddl. Qed.

Lemma : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.

Proof.

move: z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry)//.
exact: ltr_pwDr.
Qed.

Lemma : x \is a fin_num -> 0 < y -> z <= x -> z < x + y.

Proof.

move: z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry,ltNyr)//.
exact: ltr_pwDr.
Qed.

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.

Section esg.
Context { : realDomainType}.
Implicit Types x : \bar R.

Definition : \bar R := if x == 0 then 0 else if x < 0 then -1 else 1.

Lemma : x = esg x * `| x |.

Proof.

rewrite /esg; have [x0|x0|->] := ltgtP x 0.
- by rewrite lte0_abs// muleNN mul1e.
- by rewrite gte0_abs// mul1e.
- by rewrite abse0 mule0.
Qed.

Lemma : x < 0 -> esg x = -1.

Proof.

by move=> x0; rewrite /esg lt_eqF// x0. Qed.

Lemma : 0 < x -> esg x = 1.

Proof.

by move=> x0; rewrite /esg gt_eqF// ltNge (ltW x0). Qed.

Lemma : esg 0 = 0

Proof.

by rewrite /esg eqxx. Qed.

End esg.

Module .

Section DualERealArithTh_realDomainType.

Import DualAddTheoryNumDomain.

Local Open Scope ereal_dual_scope.

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

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

Proof.

by rewrite dual_addeE oppe_lt0 sube_gt0 lteN2. Qed.

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

Proof.

by rewrite dual_addeE oppe_ge0 sube_le0 leeN2. Qed.

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

Proof.

by move=> ?; rewrite dual_addeE oppe_le0 suber_ge0 ?fin_numN// leeN2.
Qed.

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

Proof.

by move=> ?; rewrite dual_addeE oppe_le0 subre_ge0 ?fin_numN// leeN2.
Qed.

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

Proof.

by move=> /orP[?|?]; [rewrite dsuber_le0|rewrite dsubre_le0]. Qed.

Lemma : a < b -> x < y -> a + x < b + y.

Proof.

rewrite !dual_addeE lteN2 -lteN2 -(lteN2 y); exact: lteD. Qed.

Lemma : 0 <= y -> x <= x + y.

Proof.

rewrite dual_addeE leeNr -oppe_le0; exact: geeDl. Qed.

Lemma : 0 <= y -> x <= y + x.

Proof.

rewrite dual_addeE leeNr -oppe_le0; exact: geeDr. Qed.

Lemma : y <= 0 -> x + y <= x.

Proof.

rewrite dual_addeE leeNl -oppe_ge0; exact: leeDl. Qed.

Lemma : y <= 0 -> y + x <= x.

Proof.

rewrite dual_addeE leeNl -oppe_ge0; exact: leeDr. Qed.

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

Proof.

by rewrite -fin_numN dual_addeE lteNr; exact: gte_subl. Qed.

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

Proof.

by rewrite -fin_numN dual_addeE lteNr addeC; exact: gte_subl. Qed.

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

Proof.

by rewrite -fin_numN dual_addeE lteNl oppeK; exact: lteDl. Qed.

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

Proof.

by rewrite -fin_numN dual_addeE lteNl oppeK; exact: lteDr. Qed.

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

Proof.

by rewrite -fin_numN dual_addeE lteNl -[0]oppe0 lteNr; exact: lteDl.
Qed.

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

Proof.

by rewrite daddeC; exact: gte_dDl. Qed.

Lemma : x \is a fin_num -> (x + a < x + b) = (a < b).

Proof.

by move=> ?; rewrite !dual_addeE lteN2 lteD2lE ?fin_numN// lteN2. Qed.

Lemma : x \is a fin_num -> (a + x < b + x) = (a < b).

Proof.

move=> ?; rewrite !dual_addeE lteN2 -[RHS]lteN2.
by rewrite -[RHS](@lteD2rE _ (- x))// fin_numN.
Qed.

Lemma : x \is a fin_num -> (a + x <= b + x) = (a <= b).

Proof.

move=> ?; rewrite !dual_addeE leeN2 -[RHS]leeN2.
by rewrite -[RHS](@leeD2rE _ (- x))// fin_numN.
Qed.

Lemma : a <= b -> x + a <= x + b.

Proof.

rewrite !dual_addeE leeN2 -leeN2; exact: leeD2l. Qed.

Lemma : x \is a fin_num -> (x + a <= x + b) = (a <= b).

Proof.

by move=> ?; rewrite !dual_addeE leeN2 leeD2lE ?fin_numN// leeN2. Qed.

Lemma : a <= b -> a + x <= b + x.

Proof.

rewrite !dual_addeE leeN2 -leeN2; exact: leeD2r. Qed.

Lemma : a <= b -> x <= y -> a + x <= b + y.

Proof.

rewrite !dual_addeE leeN2 -leeN2 -(leeN2 y); exact: leeD. Qed.

Lemma : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.

Proof.

by rewrite !dual_addeE lteN2 -lteN2; exact: lte_leB. Qed.

Lemma : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.

Proof.

by move=> afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dD. Qed.

Lemma : x <= y -> t <= z -> x - z <= y - t.

Proof.

rewrite !dual_addeE leeNl oppeK -leeN2 !oppeK; exact: leeD. Qed.

Lemma : u \is a fin_num -> x < z -> u <= y -> x - y < z - u.

Proof.

by rewrite !dual_addeE lteN2 !oppeK -lteN2; exact: lte_leD. Qed.

Lemma ( : I -> \bar^d R) ( : pred I) :
(forall , P i -> f i <= g i) ->
\sum_( <- s | P i) f i <= \sum_( <- s | P i) g i.

Proof.

move=> Pfg; rewrite !dual_sumeE leeN2.
apply: lee_sum => i Pi; rewrite leeN2; exact: Pfg.
Qed.

Lemma ( : seq I) ( : {pred I}) ( : I -> \bar^d R) :
{subset Q <= P} -> {in [predD P & Q], forall , 0 <= f i} ->
\sum_( <- s | Q i) f i <= \sum_( <- s | P i) f i.

Proof.

move=> QP PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_subset => [//|i iPQ]; rewrite oppe_le0; exact: PQf.
Qed.

Lemma ( : seq I) ( : {pred I}) ( : I -> \bar^d R) :
{subset Q <= P} -> {in [predD P & Q], forall , f i <= 0} ->
\sum_( <- s | P i) f i <= \sum_( <- s | Q i) f i.

Proof.

move=> QP PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_subset => [//|i iPQ]; rewrite oppe_ge0; exact: PQf.
Qed.

Lemma ( : eqType) ( : seq I) ( : pred I)
( : I -> \bar^d R) : (forall , P i -> ~~ Q i -> 0 <= f i) ->
\sum_( <- s | P i && Q i) f i <= \sum_( <- s | P i) f i.

Proof.

move=> PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos => i Pi nQi; rewrite oppe_le0; exact: PQf.
Qed.

Lemma ( : eqType) ( : seq I) ( : pred I)
( : I -> \bar^d R) : (forall , P i -> ~~ Q i -> f i <= 0) ->
\sum_( <- s | P i) f i <= \sum_( <- s | P i && Q i) f i.

Proof.

move=> PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg => i Pi nQi; rewrite oppe_ge0; exact: PQf.
Qed.

Lemma ( : nat -> \bar^d R) ( : pred nat) :
(forall , P n -> 0 <= f n)%E ->
{homo (fun => \sum_( < n | P i) (f i)) : / (i <= j)%N >-> i <= j}.

Proof.

move=> f0 m n mlen; rewrite !dual_sumeE leeN2.
apply: (lee_sum_npos_ord (fun => - f i)%E) => [i Pi|//].
rewrite oppe_le0; exact: f0.
Qed.

Lemma ( : nat -> \bar^d R) ( : pred nat) :
(forall , P n -> f n <= 0)%E ->
{homo (fun => \sum_( < n | P i) (f i)) : / (i <= j)%N >-> j <= i}.

Proof.

move=> f0 m n mlen; rewrite !dual_sumeE leeN2.
apply: (lee_sum_nneg_ord (fun => - f i)%E) => [i Pi|//].
rewrite oppe_ge0; exact: f0.
Qed.

Lemma ( : nat -> \bar^d R) ( : pred nat) :
(forall , (m <= n)%N -> P n -> 0 <= f n) ->
{homo (fun => \sum_(m <= < n | P i) (f i)) : / (i <= j)%N >-> i <= j}.

Proof.

move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_natr => [n ? ?|//]; rewrite oppe_le0; exact: f0.
Qed.

Lemma ( : nat -> \bar^d R) ( : pred nat) :
(forall , (m <= n)%N -> P n -> f n <= 0) ->
{homo (fun => \sum_(m <= < n | P i) (f i)) : / (i <= j)%N >-> j <= i}.

Proof.

move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_natr => [n ? ?|//]; rewrite oppe_ge0; exact: f0.
Qed.

Lemma ( : nat -> \bar^d R) ( : pred nat) :
(forall , (m < n)%N -> P m -> 0 <= f m) ->
{homo (fun => \sum_(m <= < n | P i) (f i)) : / (i <= j)%N >-> j <= i}.

Proof.

move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_natl => [m ? ?|//]; rewrite oppe_le0; exact: f0.
Qed.

Lemma ( : nat -> \bar^d R) ( : pred nat) :
(forall , (m < n)%N -> P m -> f m <= 0) ->
{homo (fun => \sum_(m <= < n | P i) (f i)) : / (i <= j)%N >-> i <= j}.

Proof.

move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_natl => [m ? ?|//]; rewrite oppe_ge0; exact: f0.
Qed.

Lemma ( : choiceType) ( : {fset T}%fset) ( : pred T)
  ( : T -> \bar^d R) : {subset A <= B} ->
  {in [predD B & A], forall , P t -> 0 <= f t} ->
  \sum_( <- A | P t) f t <= \sum_( <- B | P t) f t.

Proof.

move=> AB f0; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_subfset => [//|? ? ?]; rewrite oppe_le0; exact: f0.
Qed.

Lemma ( : choiceType) ( : {fset T}%fset) ( : pred T)
  ( : T -> \bar^d R) : {subset A <= B} ->
  {in [predD B & A], forall , P t -> f t <= 0} ->
  \sum_( <- B | P t) f t <= \sum_( <- A | P t) f t.

Proof.

move=> AB f0; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr oppeK lteBlDr. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lteBrDl ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lteBlDr ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lteBlDl ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lte_subel_addr ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lte_subel_addl ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lte_suber_addr ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE lteNl lteNr lte_suber_addl ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr leeBrDr ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr leeBrDl ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr leeBlDr ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr leeBlDl ?fin_numN. Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr lee_suber_addr ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr lee_suber_addl ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr lee_subel_addr ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite !dual_addeE leeNl leeNr lee_subel_addl ?fin_numN.
Qed.

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

Proof.

by move=> ?; rewrite lte_dBrDl// dadde0. Qed.

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

Proof.

by move=> ?; rewrite lte_dsuber_addl// dadde0. Qed.

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

Proof.

by move=> /orP[?|?]; [rewrite dsuber_gt0|rewrite dsubre_gt0]. Qed.

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

Proof.

by move=> *; rewrite !dual_addeE/= muleN muleDr ?adde_defNN// !muleN.
Qed.

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

Proof.

by move=> *; rewrite -!(muleC x) dmuleDr. Qed.

Lemma : 0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x.

Proof.

by move=> *; rewrite !dual_addeE mulNe le0_muleDl ?oppe_le0 ?mulNe. Qed.

Lemma : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z.

Proof.

by move=> *; rewrite !dual_addeE muleN le0_muleDr ?oppe_le0 ?muleN. Qed.

Lemma : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x.

Proof.

by move=> *; rewrite !dual_addeE mulNe ge0_muleDl ?oppe_ge0 ?mulNe. Qed.

Lemma : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z.

Proof.

by move=> *; rewrite !dual_addeE muleN ge0_muleDr ?oppe_ge0 ?muleN. Qed.

Lemma ( : Type) ( : seq I) ( : pred I)
    ( : I -> \bar^d R) :
  (forall , P i -> 0 <= F i) ->
  (\sum_( <- s | P i) F i) * x = \sum_( <- s | P i) (F i * x).

Proof.

move=> F0; rewrite !dual_sumeE !mulNe le0_sume_distrl => [i Pi|].
- by rewrite oppe_le0 F0.
- by under eq_bigr => i _ do rewrite mulNe.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I)
    ( : I -> \bar^d R) :
  (forall , P i -> 0 <= F i) ->
  x * (\sum_( <- s | P i) F i) = \sum_( <- s | P i) (x * F i).

Proof.

by move=> F0; rewrite muleC ge0_dsume_distrl//; under eq_bigr do rewrite muleC.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I)
    ( : I -> \bar^d R) :
  (forall , P i -> F i <= 0) ->
  (\sum_( <- s | P i) F i) * x = \sum_( <- s | P i) (F i * x).

Proof.

move=> F0; rewrite !dual_sumeE mulNe ge0_sume_distrl => [i Pi|].
- by rewrite oppe_ge0 F0.
- by under eq_bigr => i _ do rewrite mulNe.
Qed.

Lemma ( : Type) ( : seq I) ( : pred I)
    ( : I -> \bar^d R) :
  (forall , P i -> F i <= 0) ->
  x * (\sum_( <- s | P i) F i) = \sum_( <- s | P i) (x * F i).

Proof.

by move=> F0; rewrite muleC le0_dsume_distrl//; under eq_bigr do rewrite muleC.
Qed.

Lemma : `|x + y| <= `|x| + `|y|.

Proof.

by move: x y => [x| |] [y| |] //; rewrite /abse -dEFinD lee_fin ler_normD.
Qed.

Lemma ( : Type) ( : seq I) ( : I -> \bar^d R) ( : pred I) :
`|\sum_( <- s | P i) F i| <= \sum_( <- s | P i) `|F i|.

Proof.

elim/big_ind2 : _ => //; first by rewrite abse0.
by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dD _ _)).
Qed.

Lemma : `|x - y| <= `|x| + `|y|.

Proof.

by move: x y => [x| |] [y| |] //; rewrite /abse -dEFinD lee_fin ler_normB.
Qed.

Lemma : left_distributive (@GRing.add (\bar^d R)) mine.

Proof.

by move=> x y z; rewrite !dual_addeE oppe_min adde_maxl oppe_max. Qed.

Lemma : right_distributive (@GRing.add (\bar^d R)) mine.

Proof.

by move=> x y z; rewrite !dual_addeE oppe_min adde_maxr oppe_max. Qed.

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

Proof.

by rewrite mule_natl ednatmulE. Qed.

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

Proof.

by rewrite mule_natr ednatmulE. Qed.

Lemma : 0 <= x -> y <= z -> y <= x + z.

Proof.

by move=> *; rewrite -[y]dadd0e lee_dD. Qed.

Lemma : 0 <= x -> y < z -> y < x + z.

Proof.

by move=> x0 /lt_le_trans; apply; rewrite lee_pdaddl. Qed.

Lemma : 0 <= x -> y <= z -> y <= z + x.

Proof.

by move=> *; rewrite daddeC lee_pdaddl. Qed.

Lemma : 0 <= x -> y < z -> y < z + x.

Proof.

by move=> *; rewrite daddeC lte_pdaddl. Qed.

Lemma : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.

Proof.

move: z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry,ltNyr)//.
exact: ltr_pwDr.
Qed.

Lemma : x \is a fin_num -> 0 < y -> z <= x -> z < x + y.

Proof.

move: z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry,ltNyr)//.
exact: ltr_pwDr.
Qed.

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.

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

Definition :=
  match x, y with
  | r%:E, s%:E => [&& (r == 0) ==> (s >= 0) & (s == 0) ==> (r >= 0)]%R
  | +oo, +oo => true
  |  -oo, -oo | +oo, -oo | -oo, +oo => false
  | r%:E, +oo | +oo, r%:E => (r > 0)%R
  | r%:E, -oo | -oo, r%:E => (r > 0)%R
  end.
Arguments inveM_def : simpl never.

Notation := (inveM_def x y)
  (format "x *^-1? y", at level 50) : ereal_scope.

Lemma : (x *^-1? y) =
  [&& (x == 0) ==> (0 <= y < +oo),
      (y == 0) ==> (0 <= x < +oo),
      (`|x| == +oo) ==> (y > 0) &
      (`|y| == +oo) ==> (x > 0)].

Proof.

rewrite /inveM_def; case: x y => [r||]//= [s||]//=;
by rewrite ?eqe ?ltry ?ltxx ?andbT// lte_fin; case: ltgtP; rewrite //= andbF.
Qed.

Lemma : reflect ((x * y)^-1 = x^-1 * y^-1) (x *^-1? y).

Proof.

rewrite /inveM_def.
case: (inveP x) => [|||r rN0]; case: (inveP y) => [|||s sN0]//=;
rewrite ?(eqxx, lexx, ltxx, mule0, mul0e, mulyy, inve0, invey)//=;
    do ?by constructor.
- by rewrite mulyr sgrV implybT andbT; case: sgrP sN0 => //=;
     rewrite (mulN1e, mul1e); constructor.
- by rewrite mulyr; case: sgrP sN0 => //=;
     rewrite (mulN1e, mul1e); constructor.
- by rewrite !mulNyr sgrV; case: sgrP sN0 => //=;
     rewrite (mulN1e, mul1e); constructor.
- by rewrite mulry sgrV implybT andTb; case: sgrP rN0 => //=;
     rewrite (mulN1e, mul1e); constructor.
- by rewrite mulry; case: sgrP rN0 => //=;
     rewrite (mulN1e, mul1e); constructor.
- by rewrite mulrNy [RHS]mulrNy sgrV; case: sgrP rN0 => //=;
     rewrite (mulN1e, mul1e); constructor.
- by rewrite !inver invfM EFinM mulf_eq0 (negPf rN0) (negPf sN0);
     constructor.
Qed.

Lemma : x *^-1? y -> (x * y)^-1 = x^-1 * y^-1.

Proof.

by move/inveMP. Qed.

Lemma : x != 0 -> y != 0 ->
x \is a fin_num -> y \is a fin_num -> x *^-1? y.

Proof.

by rewrite /inveM_def/=; case: x y => [r||]//= [s||]//= /[!eqe]/negPf-> /negPf->.
Qed.

Lemma : x != 0 -> x \is a fin_num -> x^-1 * x = 1.

Proof.

move: x => [||]// r; rewrite eqe => r0 _.
by rewrite inver (negbTE r0) -EFinM mulVf.
Qed.

Local Notation := [pred : \bar R | x >= 0].

Lemma : {in nonneg &, {mono inve : /~ x <= y}}.

Proof.

move=> x y; case: (inveP x) => [|||r]; case: (inveP y) => [|||s]//=;
rewrite ?inE ?lexx// ?lee_fin.
- by case: (ltgtP s).
- by case: (ltgtP s) => //= s_gt0 _ _ _; rewrite invr_ge0 (ltW s_gt0) leey.
- by case: (ltgtP r) => //= r_gt0; rewrite leey.
- by case: (ltgtP r) => //= r_gt0 _ _ _; rewrite invr_le0 (lt_geF).
by case: (ltgtP s 0%R); case: (ltgtP r 0%R) => // *; rewrite lef_pV2.
Qed.

Lemma : {in nonneg &, {mono inve : /~ x < y}}.

Proof.

exact: leW_nmono_in lee_pV2. Qed.

Definition := (lee_pV2, lte_pV2).

Lemma : {in nonneg &, forall , (x <= y^-1) = (y <= x^-1)}.

Proof.

move=> x y /[!inE]; case: (inveP x) => [|||r]; rewrite ?lee_fin ?ltxx//=.
- move=> _; case: (inveP y) => [|||s]; rewrite ?lexx//= lee_fin => ? s_ge0.
by rewrite lee_fin invr_ge0 s_ge0 leey.
- move=> _; case: (inveP y) => [|||s]; rewrite ?lexx//= lee_fin => sN0 s_ge0.
by rewrite lee_fin [RHS]lt_geF// lt_def sN0.
case: ltgtP => // r_gt0 _ _.
case: (inveP y) => [|||s sN0]; rewrite ?ltxx//= ?lte_fin ?lee_fin.
- by rewrite leey invr_ge0 (ltW r_gt0).
- by rewrite [LHS]lt_geF.
by case: ltgtP sN0 => // s_gt0; rewrite -lef_pV2 ?qualifE/= ?invr_gt0// invrK.
Qed.

Lemma : {in nonneg &, forall , (x < y^-1) = (y < x^-1)}.

Proof.

move=> x y /[!inE] sgt0 ygt0; rewrite !lt_def inve_pge//.
by rewrite (can2_eq inveK inveK) eq_sym.
Qed.

Lemma : {in nonneg &, forall , (x^-1 <= y) = (y^-1 <= x)}.

Proof.

by move=> x y ? ?; rewrite -lee_pV2 ?inveK// inE inve_ge0. Qed.

Lemma : {in nonneg &, forall , (x^-1 < y) = (y^-1 < x)}.

Proof.

by move=> x y ? ?; rewrite -lte_pV2 ?inveK// inE inve_ge0. Qed.

Lemma : 0 <= x -> (1 < x^-1) = (x < 1).

Proof.

by move=> x0; rewrite inve_pgt ?inve1//= inE/= ?lee01. Qed.

Lemma : 0 <= x -> (1 <= x^-1) = (x <= 1).

Proof.

by move=> x0; rewrite inve_pge ?inve1//= inE/= ?lee01. Qed.

Lemma : x \is a fin_num -> x != 0 -> x / x = 1.

Proof.

move: x => [x|//|//] _.
by rewrite eqe => x0; rewrite inver (negbTE x0) -EFinM divff.
Qed.

Lemma : x \is a fin_num -> y != -oo ->
x^-1 + y^-1 = 1 -> y = x / (x - 1).

Proof.

move=> xfin yNy; have [->|x1] := eqVneq x 1.
  rewrite subee// inve0 mul1e inve1 => /eqP.
  rewrite -addeC eq_sym -sube_eq//; first by rewrite fin_num_adde_defl.
  rewrite subee// => /eqP /esym; case: y yNy => // r _.
  rewrite inver; case: ifPn => // r0 [] /(congr1 (fun => z^-1)%R).
  by rewrite invrK invr0 => /eqP; rewrite (negbTE r0).
have [->|x0] := eqVneq x 0.
  rewrite inve0 mul0e => /eqP; rewrite addeC eq_sym -sube_eq//.
    rewrite /adde_def eqxx/= andbT negb_and/= orbT/=.
    apply: contra yNy => /eqP /(congr1 inve).
    by rewrite inveK inveNy => ->.
  rewrite eq_sym/= addeC/= => /eqP /(congr1 inve).
  by rewrite inveK// inveNy => /eqP; rewrite (negbTE yNy).
have xNy : x != -oo by move: xfin; rewrite fin_numE => /andP[].
move=> /eqP; rewrite eq_sym addeC -sube_eq//.
  by rewrite fin_num_adde_defl// fin_numV.
move=> /eqP /(congr1 inve) /=; rewrite inveK => <-.
rewrite -[X in X - _](@divee x)// -[X in _ - X]div1e -muleBl.
- by rewrite fin_numV// ?gt_eqF// ltNye.
- by rewrite fin_num_adde_defl.
move: x xfin {xNy} x1 x0 => [x| |]// _; rewrite !eqe => x1 x0.
rewrite inver/= (negbTE x0)/= -EFinD -EFinM.
rewrite inver mulf_eq0 subr_eq0 (negbTE x1)/= invr_eq0.
by rewrite (negbTE x0) invfM// invrK mulrC EFinM inver/= subr_eq0 (negbTE x1).
Qed.

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

Proof.

apply/(iffP idP) => [|].
- move: x y => [x| |] [y| |]//.
  + by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_wpDr// ltW.
  + by move=> _ e e0; rewrite leNye.
- move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//;
    [|by move: xy => /(_ _ lte01)..].
  by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
Qed.

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

Proof.

apply/(iffP idP) => [xy e|xy].
by rewrite leeBlDr//; move: e; exact/lee_addgt0Pr.
by apply/lee_addgt0Pr => e e0; rewrite -leeBlDr// xy.
Qed.

Lemma : 0 <= x ->
reflect (forall , (0 < r < 1)%R -> r%:E * x <= y) (x <= y).

Proof.

move=> x0; apply/(iffP idP) => [xy r /andP[r0 r1]|h].
  move: x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0.
  by rewrite (le_trans _ xy)// gee_pMl// ltW.
have h01 : (0 < (2^-1 : R) < 1)%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n.
move: x y => [x||] [y||] // in x0 h *; last 4 first.
- by rewrite leey.
- by have := h _ h01.
- by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
- by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0].
  by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin.
have y0 : (0 < y)%R.
  by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin.
rewrite lee_fin leNgt; apply/negP => yx.
have /h : (0 < (y + x) / (2 * x) < 1)%R.
  apply/andP; split; first by rewrite divr_gt0 // ?addr_gt0// ?mulr_gt0.
  by rewrite ltr_pdivrMr ?mulr_gt0// mul1r mulr_natl mulr2n ltrD2r.
rewrite -EFinM lee_fin invfM -mulrA divfK ?gt_eqF//.
by apply/negP; rewrite -ltNge midf_lt.
Qed.

Lemma : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x).

Proof.

Lemma : (0 < r)%R -> (y * r^-1%:E < x) = (y < x * r%:E).

Proof.

by move=> r0; rewrite muleC lte_pdivrMl// muleC. Qed.

Lemma : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y).

Proof.

Lemma : (0 < r)%R -> (x < y * r^-1%:E) = (x * r%:E < y).

Proof.

by move=> r0; rewrite muleC lte_pdivlMl// muleC. Qed.

Lemma : (r < 0)%R -> (x < y * r^-1%:E) = (y < x * r%:E).

Proof.

rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
by rewrite EFinN muleN lteNr lte_pdivrMr// EFinN muleNN.
Qed.

Lemma : (r < 0)%R -> (x < r^-1%:E * y) = (y < r%:E * x).

Proof.

by move=> r0; rewrite muleC lte_ndivlMr// muleC. Qed.

Lemma : (r < 0)%R -> (r^-1%:E * y < x) = (r%:E * x < y).

Proof.

rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
by rewrite EFinN mulNe lteNl lte_pdivlMl// EFinN muleNN.
Qed.

Lemma : (r < 0)%R -> (y * r^-1%:E < x) = (x * r%:E < y).

Proof.

by move=> r0; rewrite muleC lte_ndivrMl// muleC. Qed.

Lemma : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x).

Proof.

move=> r0; apply/idP/idP.
- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivrMl// => /ltW.
by rewrite muleA -EFinM divff ?mul1e// gt_eqF.
- rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivrMl// => /ltW.
by rewrite muleA -EFinM mulVf ?mul1e// gt_eqF.
Qed.

Lemma : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E).

Proof.

by move=> r0; rewrite muleC lee_pdivrMl// muleC. Qed.

Lemma : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y).

Proof.

move=> r0; apply/idP/idP.
- rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivlMl// => /ltW.
by rewrite muleA -EFinM divff ?mul1e// gt_eqF.
- rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivlMl// => /ltW.
by rewrite muleA -EFinM mulVf ?mul1e// gt_eqF.
Qed.

Lemma : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y).

Proof.

by move=> r0; rewrite muleC lee_pdivlMl// muleC. Qed.

Lemma : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E).

Proof.

rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
by rewrite EFinN muleN leeNr lee_pdivrMr// EFinN muleNN.
Qed.

Lemma : (r < 0)%R -> (x <= r^-1%:E * y) = (y <= r%:E * x).

Proof.

by move=> r0; rewrite muleC lee_ndivlMr// muleC. Qed.

Lemma : (r < 0)%R -> (r^-1%:E * y <= x) = (r%:E * x <= y).

Proof.

rewrite -oppr0 ltrNr => r0; rewrite -{1}(opprK r) invrN.
by rewrite EFinN mulNe leeNl lee_pdivlMl// EFinN muleNN.
Qed.

Lemma : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y).

Proof.

by move=> r0; rewrite muleC lee_ndivrMl// muleC. Qed.

Lemma : (r != 0)%R ->
((r^-1)%:E * y == x) = (y == r%:E * x).

Proof.

rewrite neq_lt => /orP[|] r0.
- by rewrite eq_le lee_ndivrMl// lee_ndivlMl// -eq_le.
- by rewrite eq_le lee_pdivrMl// lee_pdivlMl// -eq_le.
Qed.

End realFieldType_lemmas.

Module .

Import DualAddTheoryNumDomain DualAddTheoryRealDomain.

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

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

Proof.

exact: lee_addgt0Pr. Qed.

End DualRealFieldType_lemmas.

End DualAddTheoryRealField.

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

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

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

Proof.

by rewrite /= sqrtr0. Qed.

Lemma : 0 <= sqrte x.

Proof.

by case: x => [x|//|]; rewrite /= ?leey// lee_fin sqrtr_ge0. Qed.

Lemma : 0 <= y -> (sqrte x <= sqrte y) = (x <= y).

Proof.

case: x y => [x||] [y||] yge0 //=.
- exact: ler_sqrt.
- by rewrite !leey.
- by rewrite leNye lee_fin sqrtr_ge0.
Qed.

Lemma : 0 <= x -> sqrte (x * y) = sqrte x * sqrte y.

Proof.

case: x y => [x||] [y||] //= age0.
- by rewrite sqrtrM ?EFinM.
- move: age0; rewrite le_eqVlt eqe => /predU1P[<-|x0].
    by rewrite mul0e sqrte0 sqrtr0 mul0e.
  by rewrite mulry gtr0_sg ?mul1e// mulry gtr0_sg ?mul1e// sqrtr_gt0.
- move: age0; rewrite mule0 mulrNy lee_fin -sgr_ge0.
  by case: sgrP; rewrite ?mul0e ?sqrte0// ?mul1e// ler0N1.
- rewrite !mulyr; case: (sgrP y) => [->||].
  + by rewrite sqrtr0 sgr0 mul0e sqrte0.
  + by rewrite mul1e/= -sqrtr_gt0 -sgr_gt0 -lte_fin => /gt0_muley->.
  + by move=> y0; rewrite EFinN mulN1e/= ltr0_sqrtr// sgr0 mul0e.
- by rewrite mule0.
Qed.

Lemma : 0 <= x -> sqrte x ^+ 2 = x.

Proof.

case: x => [x||] xge0; rewrite expe2 ?mulyy//.
by rewrite -sqrteM// -EFinM/= sqrtr_sqr ger0_norm.
Qed.

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

Proof.

by case: x => [x||//]; rewrite /expe/= ?sqrtr_sqr// mulyy. Qed.

Lemma : 0 <= x -> (sqrte x \is a fin_num) = (x \is a fin_num).

Proof.

by case: x => [x|//|//]; rewrite !qualifE/=. Qed.

End sqrte.

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

Module .
Export DualAddTheory.
End ConstructiveDualAddTheory.

Section Itv.
Context { : numDomainType}.

Definition ( : interval int) ( : \bar R) :=
(0 >=< x)%O && (x \in map_itv (EFin \o intr) i).

Local Notation := (Itv.spec (@Itv.num_sem _)).
Local Notation R := (Itv.def (@Itv.num_sem R)).
Local Notation R := (@map_itv_bound _ R intr).

Local Notation := (Itv.spec ext_num_sem).
Local Notation := (Itv.def ext_num_sem).
Local Notation :=
(@map_itv_bound _ (\bar R) (EFin \o intr)).

Lemma ( : R) : Itv.ext_num_sem i x%:E = Itv.num_sem i x.

Proof.

by case: i => [l u]; do 2![congr (_ && _)]; [case: l | case: u]. Qed.

Lemma ( : R) : ext_num_spec i x%:E = num_spec i x.

Proof.

by case: i => [//| i]; apply: ext_num_num_sem. Qed.

Lemma ( : itv_bound R) :
(map_itv_bound EFin x <= map_itv_bound EFin y)%O = (x <= y)%O.

Proof.

by case: x y => [xb x | x] [yb y | y]. Qed.

Lemma ( : itv_bound R) ( : R) :
(map_itv_bound EFin x <= BLeft y%:E)%O = (x <= BLeft y)%O.

Proof.

rewrite -[BLeft y%:E]/(map_itv_bound EFin (BLeft y)).
by rewrite le_map_itv_bound_EFin.
Qed.

Lemma ( : R) ( : itv_bound R) :
(BRight x%:E <= map_itv_bound EFin y)%O = (BRight x <= y)%O.

Proof.

rewrite -[BRight x%:E]/(map_itv_bound EFin (BRight x)).
by rewrite le_map_itv_bound_EFin.
Qed.

Lemma ( : itv_bound int) :
(ext_num_itv_bound x <= ext_num_itv_bound y)%O = (x <= y)%O.

Proof.

rewrite !(map_itv_bound_comp EFin intr)/=.
by rewrite le_map_itv_bound_EFin le_num_itv_bound.
Qed.

Lemma ( : Itv.t) : Itv.sub x y ->
forall : \bar R, ext_num_spec x z -> ext_num_spec y z.

Proof.

case: x y => [| x] [| y] //= x_sub_y z /andP[rz]; rewrite /Itv.ext_num_sem rz/=.
move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=.
move=> /andP[lxz zux]; apply/andP; split.
- by apply: le_trans lxz; rewrite le_ext_num_itv_bound.
- by apply: le_trans zux _; rewrite le_ext_num_itv_bound.
Qed.

Section ItvTheory.
Context { : Itv.t}.
Implicit Type x : ext_num_def i.

Lemma : Itv.sub i i' ->
ext_num_spec i' x%:inum.

Proof.

by case: x => x /= /[swap] /ext_num_spec_sub; apply. Qed.

Definition ( : unify_itv i i') :=
Itv.mk (ext_widen_itv_subproof x uni).

Lemma : unify_itv i (Itv.Real `]0%Z, +oo[) -> 0%E < x%:inum :> \bar R.

Proof.

case: x => x /= /[swap] /ext_num_spec_sub /[apply] /andP[_].
by rewrite /= in_itv/= andbT.
Qed.

Lemma : unify_itv i (Itv.Real `]-oo, 0%Z[) -> x%:inum < 0%E :> \bar R.

Proof.

by case: x => x /=/[swap] /ext_num_spec_sub /[apply] /andP[_]/=; rewrite in_itv.
Qed.

Lemma : unify_itv i (Itv.Real `[0%Z, +oo[) -> 0%E <= x%:inum :> \bar R.

Proof.

case: x => x /= /[swap] /ext_num_spec_sub /[apply] /andP[_] /=.
by rewrite in_itv/= andbT.
Qed.

Lemma : unify_itv i (Itv.Real `]-oo, 0%Z]) -> x%:inum <= 0%E :> \bar R.

Proof.

by case: x => x /=/[swap] /ext_num_spec_sub /[apply] /andP[_]/=; rewrite in_itv.
Qed.

Lemma : unify_itv i (Itv.Real `]-oo, +oo[) -> (0%E >=< x%:inum)%O.

Proof.

by case: i x => [//| [l u] [[x||//] /=/andP[/= xr _]]]. Qed.

Lemma :
unify (fun => ~~ Itv.sub ix iy) (Itv.Real `[0%Z, 0%Z]) i ->
x%:inum != 0 :> \bar R.

Proof.

case: i x => [//| [l u] [x /= Px]]; apply: contra => /eqP x0 /=.
move: Px; rewrite x0 => /and3P[_ /= l0 u0]; apply/andP; split.
- by case: l l0 => [[] l |]; rewrite ?bnd_simp ?lee_fin ?lte_fin ?lerz0 ?ltrz0.
- by case: u u0 => [[] u |]; rewrite ?bnd_simp ?lee_fin ?lte_fin ?ler0z ?ltr0z.
Qed.

End ItvTheory.

End Itv.

Arguments gt0e {R i} _ {_}.
Arguments lte0 {R i} _ {_}.
Arguments ge0e {R i} _ {_}.
Arguments lee0 {R i} _ {_}.
Arguments cmp0e {R i} _ {_}.
Arguments neqe0 {R i} _ {_}.
Arguments ext_widen_itv {R i} _ {_ _}.

Definition ( : numDomainType) & phant R :=
  Itv.def (@ext_num_sem R) (Itv.Real `]0%Z, +oo[).
Notation := (@posnume _ (Phant R)) : type_scope.
Definition ( : numDomainType) & phant R :=
  Itv.def (@ext_num_sem R) (Itv.Real `[0%Z, +oo[).
Notation := (@nonnege _ (Phant R)) : type_scope.
Notation := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)
  : ereal_dual_scope.
Notation := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)
  : ereal_scope.
Notation := (@ext_widen_itv _ _
    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _)
  (only printing) : ereal_dual_scope.
Notation := (@ext_widen_itv _ _
    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _)
  (only printing) : ereal_scope.
Notation := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing)
  : ereal_dual_scope.
Notation := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing)
  : ereal_scope.
Notation := (@ext_widen_itv _ _
    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _)
  (only printing) : ereal_dual_scope.
Notation := (@ext_widen_itv _ _
    (@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _)
  (only printing) : ereal_scope.

#[export] Hint Extern 0 (is_true (0%R < _)%E) => solve [apply: gt0e] : core.
#[export] Hint Extern 0 (is_true (_ < 0%R)%E) => solve [apply: lte0] : core.
#[export] Hint Extern 0 (is_true (0%R <= _)%E) => solve [apply: ge0e] : core.
#[export] Hint Extern 0 (is_true (_ <= 0%R)%E) => solve [apply: lee0] : core.
#[export] Hint Extern 0 (is_true (0%R >=< _)%O) => solve [apply: cmp0e] : core.
#[export] Hint Extern 0 (is_true (_ != 0%R)%O) => solve [apply: neqe0] : core.

Module .

Import IntItv.
Import Instances.

Section Itv.
Context { : numDomainType}.

Local Notation := (Itv.spec (@Itv.num_sem _)).
Local Notation R := (Itv.def (@Itv.num_sem R)).
Local Notation R := (@map_itv_bound _ R intr).

Local Notation := (Itv.spec ext_num_sem).
Local Notation := (Itv.def ext_num_sem).
Local Notation := (@map_itv_bound _ (\bar R) (EFin \o intr)).

Lemma : ext_num_spec (Itv.Real `]1%Z, +oo[) (+oo : \bar R).

Proof.

by apply/and3P; rewrite /= cmp0y !bnd_simp real_ltry. Qed.

Canonical := Itv.mk (ext_num_spec_pinfty).

Lemma :
ext_num_spec (Itv.Real `]-oo, (-1)%Z[) (-oo : \bar R).

Proof.

by apply/and3P; rewrite /= cmp0Ny !bnd_simp real_ltNyr. Qed.

Canonical := Itv.mk (ext_num_spec_ninfty).

Lemma ( : num_def R i) : ext_num_spec i x%:num%:E.

Proof.

case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
by apply/and3P; split=> [//||]; [case: l lx | case: u xu].
Qed.

Canonical ( : num_def R i) := Itv.mk (ext_num_spec_EFin x).

Lemma ( : ext_num_def i) ( := Itv.real1 keep_sign i) :
num_spec r (fine x%:num : R).

Proof.

rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
apply/and3P; split; rewrite -?real_fine//.
- case: x lx {xu xr} => [x||]/=; [|by case: l => [? []|]..].
  by case: l => [[] [l |//] |//] /[!bnd_simp] => [|/ltW]/=; rewrite lee_fin;
     apply: le_trans.
- case: x xu {lx xr} => [x||]/=; [|by case: u => [? [[]|] |]..].
  by case: u => [bu [[|//] | u] |//]; case: bu => /[!bnd_simp] [/ltW|]/=;
     rewrite lee_fin// => /le_trans; apply; rewrite lerz0.
Qed.

Canonical ( : ext_num_def i) := Itv.mk (num_spec_fine x).

Lemma :
ext_num_sem (Interval l u) (+oo : \bar R) = ((l != +oo%O) && (u == +oo%O)).

Proof.

apply/and3P/andP => [[_ ly uy] | [ly uy]]; split.
- by case: l ly => -[].
- by case: u uy => -[].
- exact: cmp0y.
- case: l ly => [|[]//].
by case=> l _ /=; rewrite bnd_simp ?real_leey ?real_ltry /= realz.
- by case: u uy => -[].
Qed.

Lemma :
ext_num_sem (Interval l u) (-oo : \bar R) = ((l == -oo%O) && (u != -oo%O)).

Proof.

apply/and3P/andP => [[_ ly uy] | [ly uy]]; split.
- by case: l ly => -[].
- by case: u uy => -[].
- exact: real0.
- by case: l ly => -[].
- case: u uy => [|[]//].
by case=> u _ /=; rewrite bnd_simp ?real_leNye ?real_ltNyr /= realz.
Qed.

Lemma ( : \bar R) :
(BRight (- x) <= ext_num_itv_bound (opp_bound b))%O
= (ext_num_itv_bound b <= BLeft x)%O.

Proof.

by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz EFinN ?leeN2 // lteN2.
Qed.

Lemma ( : \bar R) :
(ext_num_itv_bound (opp_bound b) <= BLeft (- x))%O
= (BRight x <= ext_num_itv_bound b)%O.

Proof.

by case: b => [[] b | []//]; rewrite /= !bnd_simp mulrNz EFinN ?leeN2 // lteN2.
Qed.

Lemma ( : ext_num_def i) ( := Itv.real1 opp i) :
ext_num_spec r (- x%:inum : \bar R).

Proof.

rewrite {}/r; case: x => -[x||]/=;
[|by case: i => [//| [l u]]; rewrite /= ext_num_sem_y ext_num_sem_Ny;
case: l u => [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px.
by rewrite -[x]/(Itv.mk Px)%:inum num_spec_opp.
Qed.

Canonical ( : ext_num_def i) := Itv.mk (ext_num_spec_opp x).

Lemma ( : ext_num_def xi) ( : ext_num_def yi)
( := Itv.real2 add xi yi) :
ext_num_spec r (adde x%:inum y%:inum : \bar R).

Proof.

rewrite {}/r; case: x y => -[x||] + [[y||]]/=;
  [|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
       rewrite /adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
       case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px Py.
by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum num_spec_add.
Qed.

Canonical ( : ext_num_def xi) ( : ext_num_def yi) :=
Itv.mk (ext_num_spec_add x y).

Import DualAddTheory.

Lemma ( : num_def R i) : ext_num_spec i (dEFin x%:num).

Proof.

case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
by apply/and3P; split=> [//||]; [case: l lx | case: u xu].
Qed.

Canonical ( : num_def R i) := Itv.mk (ext_num_spec_dEFin x).

Lemma ( : ext_num_def xi) ( : ext_num_def yi)
( := Itv.real2 add xi yi) :
ext_num_spec r (dual_adde x%:inum y%:inum : \bar^d R).

Proof.

rewrite {}/r; case: x y => -[x||] + [[y||]]/=;
  [|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
       rewrite /dual_adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
       case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px Py.
by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum num_spec_add.
Qed.

Canonical ( : ext_num_def xi) ( : ext_num_def yi) :=
  Itv.mk (ext_num_spec_dadd x y).

Variant ( : itv_bound int) ( : \bar R) : signi -> Set :=
  | : l = BLeft 0%Z -> u = BRight 0%Z -> x = 0 ->
                  ext_sign_spec l u x (Known EqZero)
  | : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x ->
                  ext_sign_spec l u x (Known NonNeg)
  | : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 ->
                  ext_sign_spec l u x (Known NonPos)
  | : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O ->
                (0 >=< x)%O -> ext_sign_spec l u x Unknown.

Lemma ( : itv_bound int) ( : \bar R) :
    (ext_num_itv_bound l <= BLeft x)%O -> (BRight x <= ext_num_itv_bound u)%O ->
    (0 >=< x)%O ->
  ext_sign_spec l u x (sign (Interval l u)).

Proof.

case: x => [x||] xl xu xs.
- case: (@signP R l u x _ _ xs).
  + by case: l xl => -[].
  + by case: u xu => -[].
  + by move=> l0 u0 x0; apply: ISignEqZero => //; rewrite x0.
  + by move=> l0 u0 x0; apply: ISignNonNeg.
  + by move=> l0 u0 x0; apply: ISignNonPos.
  + by move=> l0 u0 x0; apply: ISignBoth.
- have uy : u = +oo%O by case: u xu => -[].
  have u0 : (BRight 0%:Z < u)%O by rewrite uy.
  case: (leP (BLeft 0%Z) l) => l0.
  + suff -> : sign (Interval l u) = Known NonNeg.
      by apply: ISignNonNeg => //; apply: le0y.
    rewrite /=/sign_boundl /sign_boundr uy/=.
    by case: eqP => [//| /eqP lneq0]; case: ltgtP l0 lneq0.
  + suff -> : sign (Interval l u) = Unknown by exact: ISignBoth.
    rewrite /=/sign_boundl /sign_boundr uy/=.
    by case: eqP l0 => [->//| /eqP leq0] /ltW->.
- have ly : l = -oo%O by case: l xl => -[].
  have l0 : (l < BLeft 0%:Z)%O by rewrite ly.
  case: (leP u (BRight 0%Z)) => u0.
  + suff -> : sign (Interval l u) = Known NonPos by exact: ISignNonPos.
    rewrite /=/sign_boundl /sign_boundr ly/=.
    by case: eqP => [//| /eqP uneq0]; case: ltgtP u0 uneq0.
  + suff -> : sign (Interval l u) = Unknown by exact: ISignBoth.
    rewrite /=/sign_boundl /sign_boundr ly/=.
    by case: eqP u0 => [->//| /eqP ueq0]; rewrite ltNge => /negbTE->.
Qed.

Lemma ( : \bar R) :
  (BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 ->
   ext_num_itv_bound b1 <= BLeft x1 ->
   ext_num_itv_bound b2 <= BLeft x2 ->
   ext_num_itv_bound (mul_boundl b1 b2) <= BLeft (x1 * x2))%O.

Proof.

move=> b10 b20 b1x1 b2x2.
have x10 : 0 <= x1.
  by case: x1 b1x1 (le_trans (eqbRL (le_ext_num_itv_bound _ _) b10) b1x1).
have x20 : 0 <= x2.
  by case: x2 b2x2 (le_trans (eqbRL (le_ext_num_itv_bound _ _) b20) b2x2).
have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have ley b1' b2' :
    (map_itv_bound EFin (num_itv_bound R (mul_boundl b1' b2'))
     <= BLeft +oo%E)%O.
  by case: b1' b2' => [[] [[| ?] | ?] | []] [[] [[| ?] | ?] | []]//=;
     rewrite bnd_simp ?real_leey ?real_ltry/= ?realz.
case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
- rewrite !(map_itv_bound_comp, map_itv_bound_EFin_le_BLeft)/=.
  exact: num_itv_mul_boundl.
- rewrite !(map_itv_bound_comp EFin intr) real_mulry//= => b1x1 _.
  case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
    by rewrite gtr0_sg ?mul1e ?bnd_simp.
  rewrite -x10 sgr0 mul0e/= map_itv_bound_EFin_le_BLeft.
  suff -> : b1 = BLeft 0%Z by case: b2 {b20}.
  apply/le_anti; rewrite b10 andbT.
  move: b1x1; rewrite map_itv_bound_EFin_le_BLeft.
  by rewrite -x10 -(mulr0z 1) num_itv_bound_le_BLeft.
- rewrite !(map_itv_bound_comp EFin intr) real_mulyr//= => _ b2x2.
  case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
    by rewrite gtr0_sg ?mul1e ?bnd_simp.
  rewrite -x20 sgr0 mul0e/= map_itv_bound_EFin_le_BLeft.
  suff -> : b2 = BLeft 0%Z by case: b1 {b10} => [[] [] []|].
  apply/le_anti; rewrite b20 andbT.
  move: b2x2; rewrite map_itv_bound_EFin_le_BLeft.
  by rewrite -x20 -(mulr0z 1) num_itv_bound_le_BLeft.
- by rewrite mulyy/= 3!map_itv_bound_comp.
Qed.

Lemma ( : \bar R) :
  (0 <= x1 -> 0 <= x2 ->
   BRight x1 <= ext_num_itv_bound b1 ->
   BRight x2 <= ext_num_itv_bound b2 ->
   BRight (x1 * x2) <= ext_num_itv_bound (mul_boundr b1 b2))%O.

Proof.

move=> x10 x20 b1x1 b2x2.
have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
- rewrite !(map_itv_bound_comp, BRight_le_map_itv_bound_EFin)/=.
  exact: num_itv_mul_boundr.
- rewrite real_mulry// => b1x1 b2x2.
  have -> : b2 = +oo%O by case: b2 b2x2 => -[].
  rewrite mul_boundrC/= map_itv_bound_comp.
  case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
  + rewrite gtr0_sg ?mul1e ?bnd_simp//.
    suff: (BRight 0%Z < b1)%O by case: b1 b1x1 => [[] [] [] |].
    move: b1x1; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
    case: b1 => [[] b1 |//]; rewrite !bnd_simp -(@ltr0z R).
    * exact/le_lt_trans/ltW.
    * exact/lt_le_trans.
  + rewrite -x10 sgr0 mul0e/= BRight_le_map_itv_bound_EFin.
    suff: (BRight 0%Z <= b1)%O by case: b1 b1x1 => [[] [] [] |].
    move: b1x1; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
    by rewrite -x10 -(@mulr0z R 1) BRight_le_num_itv_bound.
- rewrite real_mulyr// => b1x1 b2x2.
  have -> : b1 = +oo%O by case: b1 b1x1 => -[].
  rewrite /= map_itv_bound_comp.
  case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
  + rewrite gtr0_sg ?mul1e ?bnd_simp//.
    suff: (BRight 0%Z < b2)%O by case: b2 b2x2 => [[] [] [] |].
    move: b2x2; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
    case: b2 => [[] b2 |//]; rewrite !bnd_simp -(@ltr0z R).
    * exact/le_lt_trans/ltW.
    * exact/lt_le_trans.
  + rewrite -x20 sgr0 mul0e/= BRight_le_map_itv_bound_EFin.
    suff: (BRight 0%Z <= b2)%O by case: b2 b2x2 => [[] [] [] |].
    move: b2x2; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
    by rewrite -x20 -(@mulr0z R 1) BRight_le_num_itv_bound.
- rewrite mulyy/= => b1x1 b2x2.
  have -> : b1 = +oo%O by case: b1 b1x1 => -[].
  by have -> : b2 = +oo%O by case: b2 b2x2 => -[].
Qed.

Lemma ( : \bar R) :
  (0 <= x1 -> (0 >=< x2)%O -> BRight 0%Z <= b2 ->
   BRight x1 <= ext_num_itv_bound b1 ->
   BRight x2 <= ext_num_itv_bound b2 ->
   BRight (x1 * x2) <= ext_num_itv_bound (mul_boundr b1 b2))%O.

Proof.

move=> x1ge0 x2r b2ge0 lex1b1 lex2b2.
have /orP[x2ge0 | x2le0] : (0 <= x2) || (x2 <= 0).
- by case: x2 x2r {lex2b2} => [x2 /=|_|_]; rewrite ?lee_fin ?le0y ?leNy0.
- exact: ext_num_itv_mul_boundr_pos.
have : (BRight (x1 * x2) <= BRight 0%R)%O.
by have:= mule_ge0_le0 x1ge0 x2le0; case: mule.
move/le_trans; apply.
rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin/=.
rewrite -(@mulr0z R 1) BRight_le_num_itv_bound.
apply: mul_boundr_gt0 => //.
move: x1 x1ge0 lex1b1 => [x1||//]/= x1ge0; last by case: b1 => -[].
rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
rewrite -(@BRight_le_num_itv_bound R)/=.
by apply: le_trans; rewrite bnd_simp -lee_fin.
Qed.

Lemma ( : itv_bound int) :
(ext_num_itv_bound x >=< ext_num_itv_bound y)%O.

Proof.

apply/orP; rewrite !(map_itv_bound_comp EFin intr)/= !le_map_itv_bound_EFin.
exact/orP/comparable_num_itv_bound.
Qed.

Lemma ( : itv_bound int) :
ext_num_itv_bound (Order.min x y)
= Order.min (ext_num_itv_bound x) (ext_num_itv_bound y).

Proof.

have [lexy | ltyx] := leP x y; [by rewrite !minEle le_ext_num_itv_bound lexy|].
rewrite minElt -if_neg -comparable_leNgt ?le_ext_num_itv_bound ?ltW//.
exact: comparable_ext_num_itv_bound.
Qed.

Lemma ( : itv_bound int) :
ext_num_itv_bound (Order.max x y)
= Order.max (ext_num_itv_bound x) (ext_num_itv_bound y).

Proof.

have [lexy | ltyx] := leP x y; [by rewrite !maxEle le_ext_num_itv_bound lexy|].
rewrite maxElt -if_neg -comparable_leNgt ?le_ext_num_itv_bound ?ltW//.
exact: comparable_ext_num_itv_bound.
Qed.

Lemma ( : ext_num_def xi) ( : ext_num_def yi)
( := Itv.real2 mul xi yi) :
ext_num_spec r (x%:inum * y%:inum : \bar R).

Proof.

rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]].
case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]].
rewrite -/(sign (Interval xl xu)) -/(sign (Interval yl yu)).
have ns000 : ext_num_sem `[0%Z, 0%Z] (0 : \bar R).
  by apply/and3P; rewrite ?comparablexx.
have xyr : (0 >=< (x * y)%E)%O by exact: realMe.
case: (ext_signP xlx xxu xr) => xlb xub xs.
- by rewrite xs mul0e; case: (ext_signP yly yyu yr).
- case: (ext_signP yly yyu yr) => ylb yub ys.
  + by rewrite ys mule0.
  + apply/and3P; split=> //=.
    * exact: ext_num_itv_mul_boundl.
    * exact: ext_num_itv_mul_boundr_pos.
  + apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_muleN//.
    * by rewrite oppe_boundl ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
    * rewrite oppe_boundr ext_num_itv_mul_boundl ?oppe_boundl//.
      by rewrite opp_bound_ge0.
  + apply/and3P; split=> //=.
    * rewrite -[x * y]oppeK -real_muleN// oppe_boundl.
      rewrite ext_num_itv_mul_boundr -?real_fine ?oppe_cmp0 ?oppe_boundr//.
      by rewrite opp_bound_gt0 ltW.
    * by rewrite ext_num_itv_mul_boundr// ltW.
- case: (ext_signP yly yyu yr) => ylb yub ys.
  + by rewrite ys mule0.
  + apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_mulNe//.
    * by rewrite oppe_boundl ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
    * rewrite oppe_boundr ext_num_itv_mul_boundl ?oppe_boundl//.
      by rewrite opp_bound_ge0.
  + apply/and3P; split=> //=; rewrite -real_muleNN//.
    * by rewrite ext_num_itv_mul_boundl ?opp_bound_ge0 ?oppe_boundl.
    * by rewrite ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
  + apply/and3P; split=> //=; rewrite -[x * y]oppeK.
    * rewrite -real_mulNe// oppe_boundl.
      by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
    * rewrite oppeK -real_muleNN//.
      by rewrite ext_num_itv_mul_boundr ?oppe_boundr
                 ?oppe_ge0 ?oppe_cmp0 ?opp_bound_gt0// ltW.
case: (ext_signP yly yyu yr) => ylb yub ys.
- by rewrite ys mule0.
- apply/and3P; split=> //=; rewrite muleC mul_boundrC.
  + rewrite -[y * x]oppeK -real_muleN// oppe_boundl.
    rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_cmp0 ?oppe_boundr//.
    by rewrite opp_bound_gt0 ltW.
  + by rewrite ext_num_itv_mul_boundr// ltW.
- apply/and3P; split=> //=; rewrite muleC mul_boundrC.
  + rewrite -[y * x]oppeK -real_mulNe// oppe_boundl.
    by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
  + rewrite -real_muleNN// ext_num_itv_mul_boundr ?oppe_ge0
            ?oppe_cmp0 ?oppe_boundr//.
    by rewrite opp_bound_gt0 ltW.
apply/and3P; rewrite xyr/= ext_num_itv_bound_min ext_num_itv_bound_max.
rewrite (comparable_ge_min _ (comparable_ext_num_itv_bound _ _)).
rewrite (comparable_le_max _ (comparable_ext_num_itv_bound _ _)).
have [x0 | /ltW x0] : 0 <= x \/ x < 0; [|split=> //..].
  case: x xr {xlx xxu xyr xs} => [x||] /= xr.
  - by case: (comparable_leP xr) => x0; [left | right].
  - by left; rewrite le0y.
  - by right; rewrite ltNy0.
- apply/orP; right; rewrite -[x * y]oppeK -real_muleN// oppe_boundl.
  by rewrite ext_num_itv_mul_boundr ?oppe_cmp0 ?oppe_boundr// opp_bound_gt0 ltW.
- by apply/orP; right; rewrite ext_num_itv_mul_boundr// ltW.
- apply/orP; left; rewrite -[x * y]oppeK -real_mulNe// oppe_boundl.
  by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
- apply/orP; left; rewrite -real_muleNN//.
  rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_cmp0 ?oppe_boundr//.
  by rewrite opp_bound_gt0 ltW.
Qed.

Canonical ( : ext_num_def xi) ( : ext_num_def yi) :=
  Itv.mk (ext_num_spec_mul x y).

Definition ( : Itv.t) : Itv.t :=
  match i with
  | Itv.Top => Itv.Real `[0%Z, +oo[
  | Itv.Real (Interval l u) =>
    match l with
    | BRight (Posz _) | BLeft (Posz (S _)) => Itv.Real `]0%Z, +oo[
    | _ => Itv.Real `[0%Z, +oo[
    end
  end.
Arguments abse_itv /.

Lemma ( : ext_num_def i) ( := abse_itv i) :
  ext_num_spec r (`|x%:inum| : \bar R).

Proof.

have: ext_num_sem `[0%Z, +oo[ `|x%:inum|.
  apply/and3P; split; rewrite ?bnd_simp ?abse_ge0//.
  by case: x%:inum => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
have: 0 < x%:inum -> ext_num_sem `]0%Z, +oo[ `|x%:inum|.
  move=> xgt0; apply/and3P; split; rewrite ?bnd_simp//.
  - by case: x%:num => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
  - case: x%:inum xgt0 => [x'|//|//]/=.
    by rewrite !lte_fin normr_gt0; apply: lt0r_neq0.
rewrite {}/r; case: i x => [//| [[[] [[//| l] | //] | //] u]] [x /=] + + _;
    move/and3P => [xr /= /[!bnd_simp]lx _]; apply.
- by apply: lt_le_trans lx; rewrite lte_fin ltr0z.
- by apply: le_lt_trans lx; rewrite lee_fin ler0z.
- by apply: lt_trans lx; rewrite lte_fin ltr0z.
Qed.

Canonical ( : ext_num_def i) := Itv.mk (ext_num_spec_abse x).

Lemma :
  (ext_num_itv_bound b1 <= BLeft x1)%O ->
  (ext_num_itv_bound b2 <= BLeft x2)%O ->
  (ext_num_itv_bound (Order.min b1 b2) <= BLeft (Order.min x1 x2))%O.

Proof.

case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- have sb1_le_sb2 := eqbRL (le_ext_num_itv_bound _ _) b1_le_b2.
by rewrite minElt; case: (x1 < x2)%O => [//|_]; apply: le_trans.
- have sb2_le_sb1 := eqbRL (le_ext_num_itv_bound _ _) b2_le_b1.
by rewrite minElt; case: (x1 < x2)%O => [+ _|//]; apply: le_trans.
Qed.

Lemma : (x1 >=< x2)%O ->
  (BRight x1 <= ext_num_itv_bound b1)%O ->
  (BRight x2 <= ext_num_itv_bound b2)%O ->
  (BRight (Order.min x1 x2) <= ext_num_itv_bound (Order.min b1 b2))%O.

Proof.

move=> x1_cmp_x2; case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- have sb1_le_sb2 := eqbRL (le_ext_num_itv_bound _ _) b1_le_b2.
by case: (comparable_leP x1_cmp_x2) => [//| /ltW ? + _]; apply: le_trans.
- have sb2_le_sb1 := eqbRL (le_ext_num_itv_bound _ _) b2_le_b1.
by case: (comparable_leP x1_cmp_x2) => [? _ |//]; apply: le_trans.
Qed.

Lemma ( : Itv.t) ( : ext_num_def xi) ( : ext_num_def yi)
( := Itv.real2 min xi yi) :
ext_num_spec r (Order.min x%:inum y%:inum : \bar R).

Proof.

apply: Itv.spec_real2 (Itv.P x) (Itv.P y).
case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
apply/and3P; split.
- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
  + by move=> ? ?; apply: comparable_minr.
  + by move=> ? ?; rewrite real_miney.
  + by move=> ? ?; rewrite real_minNye.
- exact: ext_min_itv_boundl_spec.
- by apply: ext_min_itv_boundr_spec => //; apply: ereal_comparable.
Qed.

Lemma : (x1 >=< x2)%O ->
  (ext_num_itv_bound b1 <= BLeft x1)%O ->
  (ext_num_itv_bound b2 <= BLeft x2)%O ->
  (ext_num_itv_bound (Order.max b1 b2) <= BLeft (Order.max x1 x2))%O.

Proof.

move=> x1_cmp_x2.
case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- case: (comparable_leP x1_cmp_x2) => [//| /ltW ? _ sb2_x2].
exact: le_trans sb2_x2 _.
- case: (comparable_leP x1_cmp_x2) => [? sb1_x1 _ |//].
exact: le_trans sb1_x1 _.
Qed.

Lemma :
  (BRight x1 <= ext_num_itv_bound b1)%O ->
  (BRight x2 <= ext_num_itv_bound b2)%O ->
  (BRight (Order.max x1 x2) <= ext_num_itv_bound (Order.max b1 b2))%O.

Proof.

case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- have sb1_le_sb2 := eqbRL (@le_ext_num_itv_bound R _ _) b1_le_b2.
by rewrite maxElt; case: ifP => [//|_ ? _]; apply: le_trans sb1_le_sb2.
- have sb2_le_sb1 := eqbRL (@le_ext_num_itv_bound R _ _) b2_le_b1.
by rewrite maxElt; case: ifP => [_ _ ?|//]; apply: le_trans sb2_le_sb1.
Qed.

Lemma ( : Itv.t) ( : ext_num_def xi) ( : ext_num_def yi)
( := Itv.real2 max xi yi) :
ext_num_spec r (Order.max x%:inum y%:inum : \bar R).

Proof.

apply: Itv.spec_real2 (Itv.P x) (Itv.P y).
case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
apply/and3P; split.
- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
  + by move=> ? ?; apply: comparable_maxr.
  + by move=> ? ?; rewrite real_maxey.
  + by move=> ? ?; rewrite real_maxNye.
- by apply: ext_max_itv_boundl_spec => //; apply: ereal_comparable.
- exact: ext_max_itv_boundr_spec.
Qed.

Canonical := MinMaxTyp ext_num_spec_min ext_num_spec_max.

End Itv.

End ItvInstances.
Export (canonicals) ItvInstances.

Section MorphNum.
Context { : numDomainType} { : Itv.t}.
Local Notation := (Itv.def (@ext_num_sem R) i).
Implicit Types (a : \bar R).

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

Proof.

by rewrite -abse_eq0. Qed.

End MorphNum.

Section MorphReal.
Context { : numDomainType} { : interval int}.
Implicit Type x : (Itv.def (@ext_num_sem R) (Itv.Real xi)).
Implicit Type y : (Itv.def (@ext_num_sem R) (Itv.Real yi)).

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

Proof.

by rewrite -comparable_le_max// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_ge_max// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_le_min// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_ge_min// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_lt_max// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_gt_max// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_lt_min// ereal_comparable. Qed.

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

Proof.

by rewrite -comparable_gt_min// ereal_comparable. Qed.

End MorphReal.

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

Lemma ( : numDomainType) ( : \bar R) : 0 < x ->
  posnume_spec x x (x == 0) (0 <= x) (0 < x).

Proof.

case: x => [x|_|//]; last by rewrite le0y lt0y; exact: IsPinftyPosnume.
rewrite lte_fin lee_fin eqe => x_gt0.
rewrite x_gt0 (ltW x_gt0) (negbTE (lt0r_neq0 x_gt0)).
exact: IsRealPosnume (PosNum x_gt0).
Qed.

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

Lemma ( : numDomainType) ( : \bar R) : 0 <= x ->
nonnege_spec x x (0 <= x).

Proof.

case: x => [x|_|//]; last by rewrite le0y; exact: IsPinftyNonnege.
by rewrite lee_fin => /[dup] x_ge0 ->; exact: IsRealNonnege (NngNum x_ge0).
Qed.

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

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

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

Proof.

rewrite normrM normfV// ltr_pdivrMr // ?mul1r//; first by rewrite gtr0_norm.
by rewrite [ltRHS]gtr0_norm ?ltrDr// ltr_pwDl.
Qed.

Lemma : (`|contract x| <= 1)%R.

Proof.

by case: x => [r| |] /=; rewrite ?normrN1 ?normr1 // (ltW (contract_lt1 _)).
Qed.

Lemma : contract 0 = 0%R.

Proof.

by rewrite /contract/= mul0r. Qed.

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

Proof.

by case: x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed.

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

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

Proof.

by move=> r1; rewrite /expand r1. Qed.

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

Proof.

rewrite /expand; case: ifPn => [r1|].
rewrite ifF; [apply/negbTE|by rewrite ifT // -lerNr].
by rewrite -ltNge -(opprK r) -ltrNl (lt_le_trans _ r1) // -subr_gt0 opprK.
rewrite -ltNge => r1; case: ifPn; rewrite lerNl opprK; [by move=> ->|].
by rewrite -ltNge leNgt => ->; rewrite leNgt -ltrNl r1 /= mulNr normrN.
Qed.

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

Proof.

by rewrite lerNr => /expand1/eqP; rewrite expandN eqe_oppLR => /eqP.
Qed.

Lemma : expand 0%R = 0.

Proof.

by rewrite /expand leNgt ltr01 /= oppr_ge0 leNgt ltr01 /= mul0r. Qed.

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

Proof.

move=> r; rewrite inE le_eqVlt => /orP[|r1].
  rewrite eqr_norml => /andP[/orP[]/eqP->{r}] _;
    by [rewrite expand1|rewrite expandN1].
rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : (r1) => -> -> /=.
have r_pneq0 : (1 + r / (1 - r) != 0)%R.
  rewrite -[X in (X + _)%R](@divff _ (1 - r)%R) -?mulrDl.
    by rewrite subr_eq0 eq_sym lt_eqF // ltr_normlW.
  by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW.
have r_nneq0 : (1 - r / (1 + r) != 0)%R.
  rewrite -[X in (X + _)%R](@divff _ (1 + r)%R) -?mulrBl.
    by rewrite addrC addr_eq0 gt_eqF // ltrNnormlW.
  by rewrite addrK mulf_neq0// invr_eq0 addr_eq0 -eqr_oppLR lt_eqF// ltrNnormlW.
wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0.
  have [r0|r0] := lerP 0 r; first by rewrite wlog_r0.
  move: (wlog_r0 (- r)%R).
  rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)).
  by move/oppr_inj.
rewrite /contract !ger0_norm //.
  by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm.
apply: (@mulIf _ (1 + r / (1 - r))%R); rewrite // divfK//.
rewrite -[X in (X + _ / _)%R](@divff _ (1 - r)%R) -?mulrDl ?subrK ?div1r //.
by rewrite subr_eq0 eq_sym lt_eqF // ltr_normlW.
Qed.

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

Proof.

apply: le_mono; move=> -[r0 | | ] [r1 | _ | _] //=.
- rewrite lte_fin => r0r1; rewrite ltr_pdivrMr ?ltr_wpDr//.
  rewrite mulrAC ltr_pdivlMr ?ltr_wpDr// 2?mulrDr 2?mulr1.
  have [r10|?] := ler0P r1; last first.
    rewrite ltr_leD // mulrC; have [r00|//] := ler0P r0.
    by rewrite (@le_trans _ _ 0%R) // ?pmulr_rle0// mulr_ge0// ?oppr_ge0// ltW.
  have [?|r00] := ler0P r0; first by rewrite ltr_leD // 2!mulrN mulrC.
  by move: (le_lt_trans r10 (lt_trans r00 r0r1)); rewrite ltxx.
- by rewrite ltr_pdivrMr ?ltr_wpDr// mul1r ltr_pwDl // ler_norm.
- rewrite ltr_pdivlMr ?mulN1r ?ltr_wpDr// => _.
  by rewrite ltrNl ltr_pwDl // ler_normr lexx orbT.
Qed.

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

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

Proof.

exact: can_mono_in (onW_can_in predT expandK) _ (in2W le_contract). Qed.

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

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

Proof.

by move=> r1; rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : r1 => -> ->.
Qed.

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

Proof.

move=> x y xy; have [x1|] := lerP `|x| 1.
  have [y_le1|/ltW /expand1->] := leP y 1%R; last by rewrite leey.
  rewrite le_expand_in ?inE// ler_norml y_le1 (le_trans _ xy)//.
  by rewrite lerNl (ler_normlP _ _ _).
rewrite ltr_normr => /orP[|] x1; last first.
  by rewrite expandN1 // ?leNye // lerNr ltW.
by rewrite expand1; [exact: ltW | rewrite expand1 // (le_trans _ xy) // ltW].
Qed.

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

Proof.

by rewrite /expand; case: ifP => //; case: ifP. Qed.

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

Proof.

rewrite /expand; case: ifP => /= r1; last by case: ifP.
by apply/esym/negbTE; rewrite -ltNge (lt_le_trans _ r1) // -subr_gt0 opprK.
Qed.

End contract_expand.

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

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

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

Proof.

by move=> e0; rewrite /ereal_ball subrr normr0. Qed.

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

Proof.

by rewrite /ereal_ball distrC. Qed.

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

Proof.

rewrite /ereal_ball => h1 h2; rewrite -[X in (X - _)%R](subrK (contract y)).
by rewrite -addrA (le_lt_trans (ler_normD _ _)) // ltrD.
Qed.

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

Proof.

by rewrite /ereal_ball 2!contractN opprK -opprB normrN addrC. Qed.

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

Proof.

move=> e2; rewrite /ereal_ball /= (le_lt_trans _ e2) // -opprB normrN opprK.
rewrite (le_trans (ler_normD _ _)) // normr1 -lerBrDr.
by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1)%R // addrK.
Qed.

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

Proof.

move=> re1; rewrite /ereal_ball; rewrite [contract +oo]/= ler0_norm.
by rewrite subr_le0; case/ler_normlP: (contract_le1 r%:E).
by rewrite opprB ltrBlDl.
Qed.

End ereal_PseudoMetric.

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

Proof.

move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
- move: a b ltax ltxb; abstract: wlog. (*BUG*)
  move=> {}a {}b ltxa ltxb.
  have m_gt0 : (Num.min ((r - a) / 2) ((b - r) / 2) > 0)%R.
    by rewrite lt_min !divr_gt0 // ?subr_gt0.
  exists (PosNum m_gt0) => y //=; rewrite lt_min !ltr_distl.
  move=> /andP[/andP[ay _] /andP[_ yb]].
  rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.
    by rewrite -subr_gt0 addrAC {1}[(r - a)%R]splitr addrK divr_gt0 ?subr_gt0.
  rewrite -subr_gt0 opprD addrA {1}[(b - r)%R]splitr addrK.
  by rewrite divr_gt0 ?subr_gt0.
- have [//||d dP] := wlog a (r + 1)%R; rewrite ?lte_fin ?ltrDl //.
  by exists d => y /dP /andP[->] /= /lt_le_trans; apply; rewrite leey.
- have [//||d dP] := wlog (r - 1)%R b; rewrite ?lte_fin ?gtrDl ?ltrN10 //.
  by exists d => y /dP /andP[_ ->] /=; rewrite ltNyr.
- by exists 1%:pos%R => ? ?; rewrite ltNyr ltry.
Qed.

Files

Module mathcomp.reals.constructive_ereal