(* This file is a modification of an eponymous file from the CoqApprox        *)
(* library. The header of the original file is reproduced below. Changes are  *)
(* part of the analysis library and enjoy the same licence as this library.   *)

Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
Require Import Rtrigo1 Reals.
From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.
Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]
Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]
Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]
Notation "_ ^ _" was already used in scope nat_scope.
[notation-overridden,parsing]
New coercion path [GRing.subring_closedM;
                   GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
                   GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing 
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.sdivr_closed_div;
                   GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing 
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.subalg_closedBM;
                   GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing 
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divring_closed_div;
                   GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing 
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.divalg_closedBdiv;
                   GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing 
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker]
New coercion path [GRing.Pred.subring_smul;
                   GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing 
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope R_scope.

Lemma Req_EM_T (r1 r2 : R) : {r1 = r2} + {r1 <> r2}.
r1, r2: R
{r1 = r2} + {r1 <> r2}
Proof.
2
case: (total_order_T r1 r2) => [[r1Lr2 | <-] | r1Gr2].
5
r1Lr2: r1 < r2
6
4
{r1 = r1} + {r1 <> r1}
5
r1Gr2: r2 < r1
6
-
9 by right=> r1Er2; case: (Rlt_irrefl r1); rewrite {2}r1Er2.
4
f
10
-
15 by left.
11
6
by right=> r1Er2; case: (Rlt_irrefl r1); rewrite {1}r1Er2.
Qed.

Definition eqr (r1 r2 : R) : bool :=
  if Req_EM_T r1 r2 is left _ then true else false.

Lemma eqrP : Equality.axiom eqr.
Equality.axiom eqr
Proof.
1d
by move=> r1 r2; rewrite /eqr; case: Req_EM_T=> H; apply: (iffP idP).
Qed.

Canonical R_eqMixin := EqMixin eqrP.
Canonical R_eqType := Eval hnf in EqType R R_eqMixin.

Fact inhR : inhabited R.
inhabited R
Proof.
22 exact: (inhabits 0). Qed.

Definition pickR (P : pred R) (n : nat) :=
  let x := epsilon inhR P in if P x then Some x else None.

Fact pickR_some P n x : pickR P n = Some x -> P x.
P: pred R
n: nat
x: R
pickR P n = Some x -> P x
Proof.
27 by rewrite /pickR; case: (boolP (P _)) => // Px [<-]. Qed.

Fact pickR_ex (P : pred R) :
  (exists x : R, P x) -> exists n, pickR P n.
2a
(exists x : R, P x) -> exists n : nat, pickR P n
Proof.
30 by rewrite /pickR; move=> /(epsilon_spec inhR)->; exists 0%N. Qed.

Fact pickR_ext (P Q : pred R) : P =1 Q -> pickR P =1 pickR Q.
P, Q: pred R
P =1 Q -> pickR P =1 pickR Q
Proof.
36
move=> PEQ n; rewrite /pickR; set u := epsilon _ _; set v := epsilon _ _.
39
PEQ: P =1 Q
2b
u:= epsilon inhR (fun x : R => P x): R
v:= epsilon inhR (fun x : R => Q x): R
(if P u then Some u else None) =
(if Q v then Some v else None)
suff->: u = v by rewrite PEQ.
3f
u = v
by congr epsilon; apply: functional_extensionality=> x; rewrite PEQ.
Qed.

Definition R_choiceMixin : choiceMixin R :=
  Choice.Mixin pickR_some pickR_ex pickR_ext.

Canonical R_choiceType := Eval hnf in ChoiceType R R_choiceMixin.

Fact RplusA : associative (Rplus).
associative Rplus
Proof.
49 by move=> *; rewrite Rplus_assoc. Qed.

Definition R_zmodMixin := ZmodMixin RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Canonical R_zmodType := Eval hnf in ZmodType R R_zmodMixin.

Fact RmultA : associative (Rmult).
associative Rmult
Proof.
4e by move=> *; rewrite Rmult_assoc. Qed.

Fact R1_neq_0 : R1 != R0.
R1 != R0
Proof.
53 by apply/eqP/R1_neq_R0. Qed.

Definition R_ringMixin := RingMixin RmultA Rmult_1_l Rmult_1_r
  Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.

Canonical R_ringType := Eval hnf in RingType R R_ringMixin.
Canonical R_comRingType := Eval hnf in ComRingType R Rmult_comm.

Import Monoid.

Canonical Radd_monoid := Law RplusA Rplus_0_l Rplus_0_r.
Canonical Radd_comoid := ComLaw Rplus_comm.

Canonical Rmul_monoid := Law RmultA Rmult_1_l Rmult_1_r.
Canonical Rmul_comoid := ComLaw Rmult_comm.

Canonical Rmul_mul_law := MulLaw Rmult_0_l Rmult_0_r.
Canonical Radd_add_law := AddLaw Rmult_plus_distr_r Rmult_plus_distr_l.

Definition Rinvx r := if (r != 0) then / r else r.

Definition unit_R r := r != 0.

Lemma RmultRinvx : {in unit_R, left_inverse 1 Rinvx Rmult}.
{in unit_R, left_inverse 1 Rinvx Rmult}
Proof.
58
move=> r; rewrite -topredE /unit_R /Rinvx => /= rNZ /=.
r: R_eqType
rNZ: r != 0
(if r != 0 then / r else r) * r = 1
by rewrite rNZ Rinv_l //; apply/eqP.
Qed.

Lemma RinvxRmult : {in unit_R, right_inverse 1 Rinvx Rmult}.
{in unit_R, right_inverse 1 Rinvx Rmult}
Proof.
64
move=> r; rewrite -topredE /unit_R /Rinvx => /= rNZ /=.
5f
r * (if r != 0 then / r else r) = 1
by rewrite rNZ Rinv_r //; apply/eqP.
Qed.

Lemma intro_unit_R x y : y * x = 1 /\ x * y = 1 -> unit_R x.
x, y: R
y * x = 1 /\ x * y = 1 -> unit_R x
Proof.
6d
move=> [yx_eq1 _]; apply: contra_eqN yx_eq1 => /eqP->.
6f
y * 0 != 1
by rewrite Rmult_0_r eq_sym R1_neq_0.
Qed.

Lemma Rinvx_out : {in predC unit_R, Rinvx =1 id}.
{in predC unit_R, Rinvx =1 id}
Proof.
78 by move=> x; rewrite inE/= /Rinvx -if_neg => ->. Qed.

Definition R_unitRingMixin :=
  UnitRingMixin RmultRinvx RinvxRmult intro_unit_R Rinvx_out.

Canonical R_unitRing :=
  Eval hnf in UnitRingType R R_unitRingMixin.

Canonical R_comUnitRingType :=
  Eval hnf in [comUnitRingType of R].

Lemma R_idomainMixin x y : x * y = 0 -> (x == 0) || (y == 0).
6f
x * y = 0 -> (x == 0) || (y == 0)
Proof.
7d by move=> /Rmult_integral []->; rewrite eqxx ?orbT. Qed.

Canonical R_idomainType := Eval hnf in IdomainType R R_idomainMixin.

Lemma R_fieldMixin : GRing.Field.mixin_of [unitRingType of R].
GRing.Field.mixin_of [unitRingType of R]
Proof.
82 by done. Qed.

Definition R_fieldIdomainMixin := FieldIdomainMixin R_fieldMixin.

Canonical R_fieldType := FieldType R R_fieldMixin.

Definition Rleb r1 r2 := if Rle_dec r1 r2 is left _ then true else false.
Definition Rltb r1 r2 := Rleb r1 r2 && (r1 != r2).
Definition Rgeb r1 r2 := Rleb r2 r1.
Definition Rgtb r1 r2 := Rltb r2 r1.

Lemma RlebP r1 r2 : reflect (r1 <= r2) (Rleb r1 r2).
4
reflect (r1 <= r2) (Rleb r1 r2)
Proof.
87 by rewrite /Rleb; apply: (iffP idP); case: Rle_dec. Qed.

Lemma RltbP r1 r2 : reflect (r1 < r2) (Rltb r1 r2).
4
reflect (r1 < r2) (Rltb r1 r2)
Proof.
8c
rewrite /Rltb /Rleb; apply: (iffP idP); case: Rle_dec=> //=.
4
r1 <= r2 -> r1 != r2 -> r1 < r2
4
r1 <= r2 -> r1 < r2 -> r1 != r2
4
~ r1 <= r2 -> r1 < r2 -> false
-
91 by case=> // r1Er2 /eqP[].
4
96
97
-
9b by move=> _ r1Lr2; apply/eqP/Rlt_not_eq.
4
98
by move=> Nr1Lr2 r1Lr2; case: Nr1Lr2; left.
Qed.

(*
Ltac toR := rewrite /GRing.add /GRing.opp /GRing.zero /GRing.mul /GRing.inv
  /GRing.one //=.
*)

Section ssreal_struct.

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Local Open Scope R_scope.

Lemma Rleb_norm_add x y : Rleb (Rabs (x + y)) (Rabs x + Rabs y).
6f
Rleb (Rabs (x + y)) (Rabs x + Rabs y)
Proof.
a3 by apply/RlebP/Rabs_triang. Qed.

Lemma addr_Rgtb0 x y : Rltb 0 x -> Rltb 0 y -> Rltb 0 (x + y).
6f
Rltb 0 x -> Rltb 0 y -> Rltb 0 (x + y)
Proof.
a8 by move/RltbP=> Hx /RltbP Hy; apply/RltbP/Rplus_lt_0_compat. Qed.

Lemma Rnorm0_eq0 x : Rabs x = 0 -> x = 0.
2c
Rabs x = 0 -> x = 0
Proof.
ad by move=> H; case: (x == 0) /eqP=> // /Rabs_no_R0. Qed.

Lemma Rleb_leVge x y : Rleb 0 x -> Rleb 0 y -> (Rleb x y) || (Rleb y x).
6f
Rleb 0 x -> Rleb 0 y -> Rleb x y || Rleb y x
Proof.
b3
move/RlebP=> Hx /RlebP Hy; case: (Rlt_le_dec x y).
70
Hx: 0 <= x
Hy: 0 <= y
x < y -> Rleb x y || Rleb y x
ba
y <= x -> Rleb x y || Rleb y x
by move/Rlt_le/RlebP=> ->.
ba
c0
by move/RlebP=> ->; rewrite orbT.
Qed.

Lemma RnormM : {morph Rabs : x y / x * y}.
{morph Rabs : x y / x * y}
exact: Rabs_mult. Qed.

Lemma Rleb_def x y : (Rleb x y) = (Rabs (y - x) == y - x).
6f
Rleb x y = (Rabs (y - x) == y - x)
apply/(sameP (RlebP x y))/(iffP idP)=> [/eqP H| /Rle_minus H].
70
H: Rabs (y - x) = y - x
x <= y
70
H: x - y <= 0
Rabs (y - x) == y - x
  apply: Rminus_le; rewrite -Ropp_minus_distr.
cf
- (y - x) <= 0
d2
  apply/Rge_le/Ropp_0_le_ge_contravar.
cf
0 <= y - x
d2
  by rewrite -H; apply: Rabs_pos.
d4
d6
apply/eqP/Rabs_pos_eq.
d4
de
rewrite -Ropp_minus_distr.
d4
0 <= - (x - y)
by apply/Ropp_0_ge_le_contravar/Rle_ge.
Qed.

Lemma Rltb_def x y : (Rltb x y) = (y != x) && (Rleb x y).
6f
Rltb x y = (y != x) && Rleb x y
apply/(sameP (RltbP x y))/(iffP idP).
6f
(y != x) && Rleb x y -> x < y
6f
x < y -> (y != x) && Rleb x y
  case/andP=> /eqP H /RlebP/Rle_not_gt H2.
70
H: y <> x
H2: ~ x > y
x < y
f1
  by case: (Rtotal_order x y)=> // [][] // /esym.
6f
f3
move=> H; apply/andP; split; [apply/eqP|apply/RlebP].
70
H: x < y
y <> x
101
d1
  exact: Rgt_not_eq.
101
d1
exact: Rlt_le.
Qed.

Definition R_numMixin := NumMixin Rleb_norm_add addr_Rgtb0 Rnorm0_eq0
                                  Rleb_leVge RnormM Rleb_def Rltb_def.
Canonical R_porderType := POrderType ring_display R R_numMixin.
Canonical R_numDomainType := NumDomainType R R_numMixin.
Canonical R_normedZmodType := NormedZmodType R R R_numMixin.

Lemma RleP : forall x y, reflect (Rle x y) (x <= y)%R.
forall x y : R, reflect (x <= y) (x <= y)%R
Proof.
10a exact: RlebP. Qed.
Lemma RltP : forall x y, reflect (Rlt x y) (x < y)%R.
forall x y : R, reflect (x < y) (x < y)%R
Proof.
10f exact: RltbP. Qed.
(* :TODO: *)
(* Lemma RgeP : forall x y, reflect (Rge x y) (x >= y)%R. *)
(* Proof. exact: RlebP. Qed. *)
(* Lemma RgtP : forall x y, reflect (Rgt x y) (x > y)%R. *)
(* Proof. exact: RltbP. Qed. *)

Canonical R_numFieldType := [numFieldType of R].

Lemma Rreal_axiom (x : R) : (0 <= x)%R || (x <= 0)%R.
af
(0 <= x)%R || (x <= 0)%R
Proof.
114
case: (Rle_dec 0 x)=> [/RleP ->|] //.
af
~ 0 <= x -> (0 <= x)%R || (x <= 0)%R
by move/Rnot_le_lt/Rlt_le/RleP=> ->; rewrite orbT.
Qed.

Lemma R_total : totalPOrderMixin R_porderType.
totalPOrderMixin R_porderType
Proof.
11d
move=> x y; case: (Rle_lt_dec x y) => [/RleP -> //|/Rlt_le/RleP ->];
  by rewrite orbT.
Qed.

Canonical R_latticeType := LatticeType R R_total.
Canonical R_distrLatticeType := DistrLatticeType R R_total.
Canonical R_orderType := OrderType R R_total.
Canonical R_realDomainType := [realDomainType of R].
Canonical R_realFieldType := [realFieldType of R].

Lemma Rarchimedean_axiom : Num.archimedean_axiom R_numDomainType.
Num.archimedean_axiom R_numDomainType
Proof.
122
move=> x; exists (Z.abs_nat (up x) + 2)%N.
x: R_numDomainType
(`|x| < (Z.abs_nat (up x) + 2)%:R)%R
have [Hx1 Hx2]:= (archimed x).
12a
Hx1: IZR (up x) > x
Hx2: IZR (up x) - x <= 1
12b
have Hz (z : Z): z = (z - 1 + 1)%Z by rewrite Zplus_comm Zplus_minus.
12a
130
131
Hz: forall z : Z, z = (z - 1 + 1)%Z
12b
have Zabs_nat_Zopp z : Z.abs_nat (- z)%Z = Z.abs_nat z by case: z.
12a
130
131
136
Zabs_nat_Zopp: forall z : Z,
Z.abs_nat (- z) = Z.abs_nat z
12b
apply/RltbP/Rabs_def1.
13a
x < ((Z.abs_nat (up x) + 2)%:R)%R
13a
- ((Z.abs_nat (up x) + 2)%:R)%R < x
  apply: (Rlt_trans _ ((Z.abs_nat (up x))%:R)%R); last first.
13a
((Z.abs_nat (up x))%:R)%R <
((Z.abs_nat (up x) + 2)%:R)%R
13a
x < ((Z.abs_nat (up x))%:R)%R
141
    rewrite -[((Z.abs_nat _)%:R)%R]Rplus_0_r mulrnDr.
13a
((Z.abs_nat (up x))%:R)%R + 0 <
((Z.abs_nat (up x))%:R + 2)%R
147
    by apply/Rplus_lt_compat_l/Rlt_0_2.
13a
149
140
  apply: (Rlt_le_trans _ (IZR (up x)))=> //.
13a
IZR (up x) <= ((Z.abs_nat (up x))%:R)%R
140
  elim/(well_founded_ind (Zwf_well_founded 0)): (up x) => z IHz.
12a
130
131
136
13b
z: Z
IHz: forall y : Z,
Zwf 0 y z -> IZR y <= ((Z.abs_nat y)%:R)%R
IZR z <= ((Z.abs_nat z)%:R)%R
140
  case: (Z_lt_le_dec 0 z) => [zp | zn].
12a
130
131
136
13b
159
15a
zp: (0 < z)%Z
15b
12a
130
131
136
13b
159
15a
zn: (z <= 0)%Z
15b
141
    rewrite [z]Hz plus_IZR Zabs_nat_Zplus //; last exact: Zlt_0_le_0_pred.
15f
IZR (z - 1) + 1 <=
((Z.abs_nat (z - 1) + Z.abs_nat 1)%coq_nat%:R)%R
161
    rewrite plusE mulrnDr.
15f
IZR (z - 1) + 1 <=
((Z.abs_nat (z - 1))%:R + (Z.abs_nat 1)%:R)%R
161
    apply/Rplus_le_compat_r/IHz; split; first exact: Zlt_le_weak.
15f
(z - 1 < z)%Z
161
    exact: Zlt_pred.
163
15b
140
  apply: (Rle_trans _ (IZR 0)); first exact: IZR_le.
163
0 <= ((Z.abs_nat z)%:R)%R
140
  by apply/RlebP/(ler0n R_numDomainType (Z.abs_nat z)).
13a
142
apply: (Rlt_le_trans _ (IZR (up x) - 1)).
13a
- ((Z.abs_nat (up x) + 2)%:R)%R < IZR (up x) - 1
13a
IZR (up x) - 1 <= x
  apply: Ropp_lt_cancel; rewrite Ropp_involutive.
13a
- (IZR (up x) - 1) < ((Z.abs_nat (up x) + 2)%:R)%R
17f
  rewrite Ropp_minus_distr /Rminus -opp_IZR -{2}(Z.opp_involutive (up x)).
13a
1 + IZR (- up x) < ((Z.abs_nat (- - up x) + 2)%:R)%R
17f
  elim/(well_founded_ind (Zwf_well_founded 0)): (- up x)%Z => z IHz .
12a
130
131
136
13b
159
IHz: forall y : Z,
Zwf 0 y z ->
1 + IZR y < ((Z.abs_nat (- y) + 2)%:R)%R
1 + IZR z < ((Z.abs_nat (- z) + 2)%:R)%R
17f
  case: (Z_lt_le_dec 0 z) => [zp | zn].
12a
130
131
136
13b
159
18e
160
18f
12a
130
131
136
13b
159
18e
164
18f
180
  rewrite [z]Hz Zabs_nat_Zopp plus_IZR.
193
1 + (IZR (z - 1) + 1) <
((Z.abs_nat (z - 1 + 1) + 2)%:R)%R
194
  rewrite Zabs_nat_Zplus //; last exact: Zlt_0_le_0_pred.
193
1 + (IZR (z - 1) + 1) <
(((Z.abs_nat (z - 1) + Z.abs_nat 1)%coq_nat + 2)%:R)%R
194
    rewrite plusE -Rplus_assoc -addnA [(_ + 2)%N]addnC addnA mulrnDr.
193
1 + IZR (z - 1) + 1 <
((Z.abs_nat (z - 1) + 2)%:R + (Z.abs_nat 1)%:R)%R
194
    apply: Rplus_lt_compat_r; rewrite -Zabs_nat_Zopp.
193
1 + IZR (z - 1) < ((Z.abs_nat (- (z - 1)) + 2)%:R)%R
194
    apply: IHz; split; first exact: Zlt_le_weak.
12a
130
131
136
13b
159
160
170
194
    exact: Zlt_pred.
196
18f
17f
  apply: (Rle_lt_trans _ 1).
196
1 + IZR z <= 1
196
1 < ((Z.abs_nat (- z) + 2)%:R)%R
180
    rewrite -{2}[1]Rplus_0_r; apply: Rplus_le_compat_l.
196
IZR z <= 0
1b2
    by rewrite -/(IZR 0); apply: IZR_le.
196
1b4
17f
  rewrite mulrnDr; apply: (Rlt_le_trans _ 2).
196
1 < 2
196
2 <= ((Z.abs_nat (- z))%:R + 2)%R
180
    by rewrite -{1}[1]Rplus_0_r; apply/Rplus_lt_compat_l/Rlt_0_1.
196
1c2
17f
  rewrite -[2]Rplus_0_l; apply: Rplus_le_compat_r.
196
0 <= ((Z.abs_nat (- z))%:R)%R
17f
  by apply/RlebP/(ler0n R_numDomainType (Z.abs_nat _)).
13a
181
apply: Rminus_le.
13a
IZR (up x) - 1 - x <= 0
rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _).
13a
IZR (up x) - x - 1 <= 0
exact: Rle_minus.
Qed.

(* Canonical R_numArchiDomainType := ArchiDomainType R Rarchimedean_axiom. *)
(* (* Canonical R_numArchiFieldType := [numArchiFieldType of R]. *) *)
(* Canonical R_realArchiDomainType := [realArchiDomainType of R]. *)
Canonical R_realArchiFieldType := ArchiFieldType R Rarchimedean_axiom.

Lemma continuity_eq f g : f =1 g -> continuity f -> continuity g.
f, g: R -> R
f =1 g -> continuity f -> continuity g
Proof.
1d6
move=> Hfg Hf x eps Heps.
1d9
Hfg: f =1 g
Hf: continuity f
x, eps: R
Heps: eps > 0
exists alp : R,
  alp > 0 /\
  (forall x0 : Base R_met,
   D_x no_cond x x0 /\ dist R_met x0 x < alp ->
   dist R_met (g x0) (g x) < eps)
have [y [Hy1 Hy2]]:= Hf x eps Heps.
1d9
1e0
1e1
1e2
1e3
y: R
Hy1: y > 0
Hy2: forall x0 : Base R_met,
D_x no_cond x x0 /\ dist R_met x0 x < y ->
dist R_met (f x0) (f x) < eps
1e4
by exists y; split=> // z; rewrite -!Hfg; exact: Hy2.
Qed.

Lemma continuity_sum (I : finType) F (P : pred I):
(forall i, P i -> continuity (F i)) ->
continuity (fun x => (\sum_(i | P i) ((F i) x)))%R.
I: finType
F: I -> R -> R
P: pred I
(forall i : I, P i -> continuity (F i)) ->
continuity (fun x : R => (\sum_(i | P i) F i x)%R)
Proof.
1ed
move=> H; elim: (index_enum I)=> [|a l IHl].
1f0
1f1
1f2
H: forall i : I, P i -> continuity (F i)
continuity
  (fun x : R => (\sum_(i <- [::] | P i) F i x)%R)
1f0
1f1
1f2
1f9
a: I
l: seq I
IHl: continuity (fun x : R => (\sum_(i <- l | P i) F i x)%R)
continuity
  (fun x : R => (\sum_(i <- (a :: l) | P i) F i x)%R)
  set f:= fun _ => _.
1f0
1f1
1f2
1f9
f:= fun H : R => (\sum_(i <- [::] | P i) F i H)%R: R -> R_zmodType
continuity f
1fb
  have Hf: (fun x=> 0) =1 f by move=> x; rewrite /f big_nil.
1f0
1f1
1f2
1f9
206
Hf: (fun=> 0) =1 f
207
1fb
  by apply: (continuity_eq Hf); exact: continuity_const.
1fd
201
set f := fun _ => _.
1f0
1f1
1f2
1f9
1fe
1ff
200
f:= fun H : R => (\sum_(i <- (a :: l) | P i) F i H)%R: R -> R_zmodType
207
case Hpa: (P a).
1f0
1f1
1f2
1f9
1fe
1ff
200
214
Hpa: P a = true
207
1f0
1f1
1f2
1f9
1fe
1ff
200
214
Hpa: P a = false
207
  have Hf: (fun x => F a x + \sum_(i <- l | P i) F i x)%R =1 f.
218
(fun x : R => (F a x + \sum_(i <- l | P i) F i x)%R) =1
f
1f0
1f1
1f2
1f9
1fe
1ff
200
214
219
Hf: (fun x : R =>
 (F a x + \sum_(i <- l | P i) F i x)%R) =1 f
207
21b
    by move=> x; rewrite /f big_cons Hpa.
224
207
21a
  apply: (continuity_eq Hf); apply: continuity_plus=> //.
224
continuity (F a)
21a
  exact: H.
21c
207
have Hf: (fun x => \sum_(i <- l | P i) F i x)%R =1 f.
21c
(fun x : R => (\sum_(i <- l | P i) F i x)%R) =1 f
1f0
1f1
1f2
1f9
1fe
1ff
200
214
21d
Hf: (fun x : R => (\sum_(i <- l | P i) F i x)%R) =1 f
207
  by move=> x; rewrite /f big_cons Hpa.
236
207
exact: (continuity_eq Hf).
Qed.

Lemma continuity_exp f n: continuity f -> continuity (fun x => (f x)^+ n)%R.
f: R -> R
2b
continuity f -> continuity (fun x : R => (f x ^+ n)%R)
Proof.
23c
move=> Hf; elim: n=> [|n IHn]; first exact: continuity_const.
23f
1e1
2b
IHn: continuity (fun x : R => (f x ^+ n)%R)
continuity (fun x : R => (f x ^+ n.+1)%R)
set g:= fun _ => _.
23f
1e1
2b
246
g:= fun H : R => (f H ^+ n.+1)%R: R -> R_ringType
continuity g
have Hg: (fun x=> f x * f x ^+ n)%R =1 g.
24b
(fun x : R => (f x * f x ^+ n)%R) =1 g
23f
1e1
2b
246
24c
Hg: (fun x : R => (f x * f x ^+ n)%R) =1 g
24d
  by move=> x; rewrite /g exprS.
254
24d
by apply: (continuity_eq Hg); exact: continuity_mult.
Qed.

Lemma Rreal_closed_axiom : Num.real_closed_axiom R_numDomainType.
Num.real_closed_axiom R_numDomainType
Proof.
25a
move=> p a b; rewrite !le_eqVlt.
p: {poly R_numDomainType}
a, b: R_numDomainType
(a == b) || (a < b)%R ->
(((p.[a])%R == 0%R) || (p.[a] < 0)%R) &&
((0%R == (p.[b])%R) || (0 < p.[b])%R) ->
exists2 x : R_numDomainType,
  (a <= x <= b)%R & root p x
case Hpa: ((p.[a])%R == 0%R).
262
263
Hpa: ((p.[a])%R == 0%R) = true
(a == b) || (a < b)%R ->
(true || (p.[a] < 0)%R) &&
((0%R == (p.[b])%R) || (0 < p.[b])%R) ->
exists2 x : R_numDomainType,
  (a <= x <= b)%R & root p x
262
263
Hpa: ((p.[a])%R == 0%R) = false
(a == b) || (a < b)%R ->
(false || (p.[a] < 0)%R) &&
((0%R == (p.[b])%R) || (0 < p.[b])%R) ->
exists2 x : R_numDomainType,
  (a <= x <= b)%R & root p x
  by move=> ? _ ; exists a=> //; rewrite lexx le_eqVlt.
26d
26f
case Hpb: ((p.[b])%R == 0%R).
262
263
26e
Hpb: ((p.[b])%R == 0%R) = true
26f
262
263
26e
Hpb: ((p.[b])%R == 0%R) = false
26f
  by move=> ? _; exists b=> //; rewrite lexx le_eqVlt andbT.
27a
26f
case Hab: (a == b).
262
263
26e
27b
Hab: (a == b) = true
true || (a < b)%R ->
(false || (p.[a] < 0)%R) &&
((0%R == (p.[b])%R) || (0 < p.[b])%R) ->
exists2 x : R_numDomainType,
  (a <= x <= b)%R & root p x
262
263
26e
27b
Hab: (a == b) = false
false || (a < b)%R ->
(false || (p.[a] < 0)%R) &&
((0%R == (p.[b])%R) || (0 < p.[b])%R) ->
exists2 x : R_numDomainType,
  (a <= x <= b)%R & root p x
  by move=> _; rewrite (eqP Hab) eq_sym Hpb (ltNge 0) /=; case/andP=> /ltW ->.
287
289
rewrite eq_sym Hpb /=; clear=> /RltbP Hab /andP [] /RltbP Hpa /RltbP Hpb.
262
263
Hab: a < b
Hpa: (p.[a])%R < 0%R
Hpb: 0%R < (p.[b])%R
exists2 x : R, (a <= x <= b)%R & root p x
suff Hcp: continuity (fun x => (p.[x])%R).
262
263
291
292
293
Hcp: continuity [eta horner p]
294
290
continuity [eta horner p]
  have [z [[Hza Hzb] /eqP Hz2]]:= IVT _ a b Hcp Hab Hpa Hpb.
262
263
291
292
293
299
z: R
Hza: a <= z
Hzb: z <= b
Hz2: (p.[z])%R == 0
294
29a
  by exists z=> //; apply/andP; split; apply/RlebP.
290
29c
rewrite -[p]coefK poly_def.
290
continuity
  [eta horner (\sum_(i < size p) p`_i *: 'X^i)]
set f := fun _ => _.
262
263
291
292
293
f:= [eta horner (\sum_(i < size p) p`_i *: 'X^i)]: R -> R_numDomainType
207
have Hf: (fun (x : R) => \sum_(i < size p) (p`_i * x^+i))%R =1 f.
2af
(fun x : R => (\sum_(i < size p) p`_i * x ^+ i)%R) =1
f
262
263
291
292
293
2b0
Hf: (fun x : R => (\sum_(i < size p) p`_i * x ^+ i)%R) =1
f
207
  move=> x; rewrite /f horner_sum.
262
263
291
292
293
2b0
2c
(\sum_(i < size p) p`_i * x ^+ i)%R =
(\sum_i (p`_i *: 'X^i).[x])%R
2b5
  by apply: eq_bigr=> i _; rewrite hornerZ hornerXn.
2b7
207
apply: (continuity_eq Hf); apply: continuity_sum=> i _.
262
263
291
292
293
2b0
2b8
i: ordinal_finType (size p)
continuity (fun x : R => (p`_i * x ^+ i)%R)
apply:continuity_scal; apply: continuity_exp=> x esp Hesp.
262
263
291
292
293
2b0
2b8
2c5
x, esp: R
Hesp: esp > 0
exists alp : R,
  alp > 0 /\
  (forall x0 : Base R_met,
   D_x no_cond x x0 /\ dist R_met x0 x < alp ->
   dist R_met x0 x < esp)
by exists esp; split=> // y [].
Qed.

Canonical R_rcfType := RcfType R Rreal_closed_axiom.
(* Canonical R_realClosedArchiFieldType := [realClosedArchiFieldType of R]. *)

End ssreal_struct.

Local Open Scope ring_scope.
From mathcomp.classical Require Import boolp classical_sets.
New coercion path [Empty.mixin; Empty.eqMixin] : Empty.class_of >-> Equality.mixin_of is ambiguous with existing 
[Empty.base; Finite.base; Choice.base] : Empty.class_of >-> Equality.mixin_of.
[ambiguous-paths,typechecker]
New coercion path [Empty.mixin; Empty.choiceMixin] : Empty.class_of >-> Choice.mixin_of is ambiguous with existing 
[Empty.base; Finite.base; Choice.mixin] : Empty.class_of >-> Choice.mixin_of.
[ambiguous-paths,typechecker]
New coercion path [Empty.mixin; Empty.countMixin] : Empty.class_of >-> Countable.mixin_of is ambiguous with existing 
[Empty.base; Finite.mixin; Finite.mixin_base] : Empty.class_of >-> Countable.mixin_of.
[ambiguous-paths,typechecker]
Require Import reals.

Section ssreal_struct_contd.
Implicit Type E : set R.

Lemma is_upper_boundE E x : is_upper_bound E x = (ubound E) x.
Proof.
rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h].
by apply/ubP => y Ey; apply/RleP/h.
Qed.

Lemma boundE E : bound E = has_ubound E.
Proof. by apply/eq_exists=> x; rewrite is_upper_boundE. Qed.

Lemma Rcondcomplete E : has_sup E -> {m | isLub E m}.
Proof.
move=> [E0 uE]; have := completeness E; rewrite boundE => /(_ uE E0)[x [E1 E2]].
exists x; split; first by rewrite -is_upper_boundE; apply: E1.
by move=> y; rewrite -is_upper_boundE => /E2/RleP.
Qed.

Lemma Rsupremums_neq0 E : has_sup E -> (supremums E !=set0)%classic.
Proof. by move=> /Rcondcomplete[x [? ?]]; exists x. Qed.

Lemma Rsup_isLub x0 E : has_sup E -> isLub E (supremum x0 E).
Proof.
have [-> [/set0P]|E0 hsE] := eqVneq E set0; first by rewrite eqxx.
have [s [Es sE]] := Rcondcomplete hsE.
split => x Ex; first by apply/ge_supremum_Nmem=> //; exact: Rsupremums_neq0.
rewrite /supremum (negbTE E0); case: xgetP => /=.
  by move=> _ -> [_ EsE]; apply/EsE.
by have [y Ey /(_ y)] := Rsupremums_neq0 hsE.
Qed.

(* :TODO: rewrite like this using (a fork of?) Coquelicot *)
(* Lemma real_sup_adherent (E : pred R) : real_sup E \in closure E. *)
Lemma real_sup_adherent x0 E (eps : R) : (0 < eps) ->
  has_sup E -> exists2 e, E e & (supremum x0 E - eps) < e.
Proof.
move=> eps_gt0 supE; set m := _ - eps; apply: contrapT=> mNsmall.
have : (ubound E) m.
  apply/ubP => y Ey.
  by have /negP := mNsmall (ex_intro2 _ _ y Ey _); rewrite -leNgt.
have [_ /(_ m)] := Rsup_isLub x0 supE.
move => m_big /m_big.
by rewrite -subr_ge0 addrC addKr oppr_ge0 leNgt eps_gt0.
Qed.

Lemma Rsup_ub x0 E : has_sup E -> (ubound E) (supremum x0 E).
Proof.
by move=> supE x Ex; apply/ge_supremum_Nmem => //; exact: Rsupremums_neq0.
Qed.

Definition real_realMixin : Real.mixin_of _ :=
  RealMixin (@Rsup_ub (0 : R)) (real_sup_adherent 0).
Canonical real_realType := RealType R real_realMixin.

Implicit Types (x y : R) (m n : nat).

(* equational lemmas about exp, sin and cos for mathcomp compat *)

(* Require Import realsum. *)

(* :TODO: One day, do this *)
(* Notation "\Sum_ i E" := (psum (fun i => E)) *)
(*  (at level 100, i ident, format "\Sum_ i  E") : ring_scope. *)

(* Definition exp x := \Sum_n (n`!)%:R^-1 * x ^ n. *)

Lemma expR0 : exp (0 : R) = 1.
Proof. by rewrite exp_0. Qed.

Lemma expRD x y : exp x * exp y = exp (x + y).
Proof. by rewrite exp_plus. Qed.

Lemma expRX x n : exp x ^+ n = exp (x *+ n).
Proof.
elim: n => [|n Ihn]; first by rewrite expr0 mulr0n exp_0.
by rewrite exprS Ihn mulrS expRD.
Qed.

Lemma sinD x y : sin (x + y) = sin x * cos y + cos x * sin y.
Proof. by rewrite sin_plus. Qed.

Lemma cosD x y : cos (x + y) = (cos x * cos y - sin x * sin y).
Proof. by rewrite cos_plus. Qed.

Lemma RplusE x y : Rplus x y = x + y. Proof. by []. Qed.

Lemma RminusE x y : Rminus x y = x - y. Proof. by []. Qed.

Lemma RmultE x y : Rmult x y = x * y. Proof. by []. Qed.

Lemma RoppE x : Ropp x = - x. Proof. by []. Qed.

Lemma RinvE x : x != 0 -> Rinv x = x^-1.
Proof. by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed.

Lemma RdivE x y : y != 0 -> Rdiv x y = x / y.
Proof. by move=> y_neq0; rewrite /Rdiv RinvE. Qed.

Lemma INRE n : INR n = n%:R.
Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed.

Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
Proof.
move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
rewrite eq_sym -(eqr_expn2 (_: 0 < 2)%N t1) //; last by apply /RleP.
rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; by apply/RleP.
Qed.

Lemma RpowE x n : pow x n = x ^+ n.
Proof. by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.

Lemma RmaxE x y : Rmax x y = Num.max x y.
Proof.
case: (lerP x y) => H; first by rewrite Rmax_right //; apply: RlebP.
by rewrite ?ltW // Rmax_left //;  apply/RlebP; move/ltW : H.
Qed.

(* useful? *)
Lemma RminE x y : Rmin x y = Num.min x y.
Proof.
case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP.
by rewrite ?ltW // Rmin_right //;  apply/RlebP; move/ltW : H.
Qed.

Section bigmaxr.
Context {R : realDomainType}.

(* bigop pour le max pour des listes non vides ? *)
#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Definition bigmaxr (r : R) s := \big[Num.max/head r s]_(i <- s) i.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0.
Proof. by rewrite /bigmaxr /= big_nil. Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x.
Proof. by rewrite /bigmaxr /= big_cons big_nil maxxx. Qed.

(* previous definition *)
#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).
Proof.
rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i).
  case: s => // ? t; rewrite big_cons /bigmaxr.
  by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
by case: s => //=; rewrite /bigmaxr big_nil.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigrmax_dflt (x y : R) s : Num.max x (\big[Num.max/x]_(j <- y :: s) j) =
  Num.max x (\big[Num.max/y]_(i <- y :: s) i).
Proof.
elim: s => /= [|h t IH] in x y *.
by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_cons (x0 x y : R) lr :
  bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).
Proof. by rewrite [y :: lr]lock /bigmaxr /= -lock big_cons bigrmax_dflt. Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_ler (x0 : R) s i :
  (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
Proof.
rewrite /bigmaxr; elim: s i => // h t IH [_|i] /=.
  by rewrite big_cons /= le_maxr lexx.
rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
Qed.

(* Compatibilité avec l'addition *)
#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_addr (x0 : R) lr (x : R) :
  bigmaxr (x0 + x) (map (fun y : R => y + x) lr) = (bigmaxr x0 lr) + x.
Proof.
rewrite /bigmaxr; case: lr => [|h t]; first by rewrite !big_nil.
elim: t h => /= [|h' t IH] h; first by rewrite ?(big_cons,big_nil) -addr_maxl.
by rewrite [in RHS]big_cons bigrmax_dflt addr_maxl -IH big_cons bigrmax_dflt.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr.
Proof.
rewrite /bigmaxr; case: lr => // h t _.
elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE maxxx.
rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
- by rewrite le_maxr lexx.
- by rewrite lt_maxr ltxx => ?; rewrite max_r ?IH // ltW.
Qed.

(* TODO: bigmaxr_morph? *)
#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_mulr (A : finType) (s : seq A) (k : R) (x : A -> R) :
  0 <= k -> bigmaxr 0 (map (fun i => k * x i) s) = k * bigmaxr 0 (map x s).
Proof.
move=> k0; elim: s => /= [|h [/=|h' t ih]].
by rewrite bigmaxr_nil mulr0.
by rewrite !bigmaxr_un.
by rewrite bigmaxr_cons {}ih bigmaxr_cons maxr_pmulr.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_index (x0 : R) lr :
  (0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N.
Proof.
rewrite /bigmaxr; case: lr => //= h t _; case: ifPn => // /negbTE H.
move: (@bigmaxr_mem x0 (h :: t) isT).
by rewrite ltnS index_mem inE /= eq_sym H.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_lerP (x0 : R) lr (x : R) :
  (0 < size lr)%N ->
  reflect (forall i, (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x).
Proof.
move=> lr_size; apply: (iffP idP) => [le_x i i_size | H].
  by apply: (le_trans _ le_x); apply: bigmaxr_ler.
by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_ltrP (x0 : R) lr (x : R) :
  (0 < size lr)%N ->
  reflect (forall i, (i < size lr)%N -> (nth x0 lr i) < x) ((bigmaxr x0 lr) < x).
Proof.
move=> lr_size; apply: (iffP idP) => [lt_x i i_size | H].
  by apply: le_lt_trans lt_x; apply: bigmaxr_ler.
by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxrP (x0 : R) lr (x : R) :
  (x \in lr /\ forall i, (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x).
Proof.
move=> [] /(nthP x0) [] j j_size j_nth x_ler; apply: le_anti; apply/andP; split.
  by apply/bigmaxr_lerP => //; apply: (leq_trans _ j_size).
by rewrite -j_nth (bigmaxr_ler _ j_size).
Qed.

(* surement à supprimer à la fin
Lemma bigmaxc_lttc x0 lc :
  uniq lc -> forall i, (i < size lc)%N -> (i != index (bigmaxc x0 lc) lc)
    -> lttc (nth x0 lc i) (bigmaxc x0 lc).
Proof.
move=> lc_uniq Hi size_i /negP neq_i.
rewrite lttc_neqAle (bigmaxc_letc _ size_i) andbT.
apply/negP => /eqP H; apply: neq_i; rewrite -H eq_sym; apply/eqP.
by apply: index_uniq.
Qed. *)

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_lerif (x0 : R) lr :
  uniq lr -> forall i, (i < size lr)%N ->
     (nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).
Proof.
move=> lr_uniq i i_size; rewrite /Num.leif (bigmaxr_ler _ i_size).
rewrite -(nth_uniq x0 i_size (bigmaxr_index _ (leq_trans _ i_size)) lr_uniq) //.
rewrite nth_index //.
by apply: bigmaxr_mem; apply: (leq_trans _ i_size).
Qed.

(* bigop pour le max pour des listes non vides ? *)
#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Definition bmaxrf n (f : {ffun 'I_n.+1 -> R}) :=
  bigmaxr (f ord0) (codom f).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bmaxrf_ler n (f : {ffun 'I_n.+1 -> R}) i :
  (f i) <= (bmaxrf f).
Proof.
move: (@bigmaxr_ler (f ord0) (codom f) (nat_of_ord i)).
rewrite /bmaxrf size_codom card_ord => H; move: (ltn_ord i); move/H.
suff -> : nth (f ord0) (codom f) i = f i; first by [].
by rewrite /codom (nth_map ord0) ?size_enum_ord // nth_ord_enum.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bmaxrf_index n (f : {ffun 'I_n.+1 -> R}) :
  (index (bmaxrf f) (codom f) < n.+1)%N.
Proof.
rewrite /bmaxrf.
rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)); last first.
  by rewrite size_codom card_ord.
by apply: bigmaxr_index; rewrite size_codom card_ord.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Definition index_bmaxrf n f := Ordinal (@bmaxrf_index n f).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma ordnat i n (ord_i : (i < n)%N) : i = Ordinal ord_i :> nat.
Proof. by []. Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma eq_index_bmaxrf n (f : {ffun 'I_n.+1 -> R}) :
  f (index_bmaxrf f) = bmaxrf f.
Proof.
move: (bmaxrf_index f).
rewrite -[X in _ (_ < X)%N]card_ord -(size_codom f) index_mem.
move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
  by rewrite (ordnat (bmaxrf_index _)) /index_bmaxrf nth_ord_enum.
by rewrite size_enum_ord; apply: bmaxrf_index.
Qed.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bmaxrf_lerif n (f : {ffun 'I_n.+1 -> R}) :
  injective f -> forall i,
     (f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f).
Proof.
by move=> inj_f i; rewrite /Num.leif bmaxrf_ler -(inj_eq inj_f) eq_index_bmaxrf.
Qed.

End bigmaxr.

End ssreal_struct_contd.

Require Import signed topology normedtype.

Section analysis_struct.

Canonical R_pointedType := [pointedType of R for pointed_of_zmodule R_ringType].
Canonical R_filteredType :=
  [filteredType R of R for filtered_of_normedZmod R_normedZmodType].
Canonical R_topologicalType : topologicalType := TopologicalType R
  (topologyOfEntourageMixin
    (uniformityOfBallMixin
      (@nbhs_ball_normE _ R_normedZmodType)
      (pseudoMetric_of_normedDomain R_normedZmodType))).
Canonical R_uniformType : uniformType :=
  UniformType R
  (uniformityOfBallMixin (@nbhs_ball_normE _ R_normedZmodType)
    (pseudoMetric_of_normedDomain R_normedZmodType)).
Canonical R_pseudoMetricType : pseudoMetricType R_numDomainType :=
  PseudoMetricType R (pseudoMetric_of_normedDomain R_normedZmodType).

(* TODO: express using ball?*)
Lemma continuity_pt_nbhs (f : R -> R) x :
  continuity_pt f x <->
  forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num).
Proof.
split=> [fcont e|fcont _/RltP/posnumP[e]]; last first.
  have [_/posnumP[d] xd_fxe] := fcont e.
  exists d%:num; split; first by apply/RltP; have := [gt0 of d%:num].
  by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC.
have /RltP egt0 := [gt0 of e%:num].
have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0.
exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney].
  by rewrite subrr normr0.
apply/RltP/dx_fxe; split; first by split=> //; apply/eqP.
by have /RltP := xyd; rewrite distrC.
Qed.

Lemma continuity_pt_cvg (f : R -> R) (x : R) :
  continuity_pt f x <-> {for x, continuous f}.
Proof.
eapply iff_trans; first exact: continuity_pt_nbhs.
apply iff_sym.
have FF : Filter (f @ x).
  by typeclasses eauto.
  (*by apply fmap_filter; apply: @filter_filter' (locally_filter _).*)
case: (@fcvg_ballP _ _ (f @ x) FF (f x)) => {FF}H1 H2.
(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *)
split => [{H2} - /H1 {}H1 eps|{H1} H].
- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
  exists x0%:num => //= Hx0' /Hx0 /=.
  by rewrite /= distrC; apply.
- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0].
  exists x0%:num => //= y /Hx0 /= {}Hx0.
  by rewrite /ball /= distrC.
Qed.

Lemma continuity_ptE (f : R -> R) (x : R) :
  continuity_pt f x <-> {for x, continuous f}.
Proof. exact: continuity_pt_cvg. Qed.

Local Open Scope classical_set_scope.

Lemma continuity_pt_cvg' f x :
  continuity_pt f x <-> f @ x^' --> f x.
Proof. by rewrite continuity_ptE continuous_withinNx. Qed.

Lemma continuity_pt_dnbhs f x :
  continuity_pt f x <->
  forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps).
Proof.
rewrite continuity_pt_cvg' (@cvgrPdist_lt _ [normedModType _ of R^o]).
exact.
Qed.

Lemma nbhs_pt_comp (P : R -> Prop) (f : R -> R) (x : R) :
  nbhs (f x) P -> continuity_pt f x -> \near x, P (f x).
Proof. by move=> Lf /continuity_pt_cvg; apply. Qed.

End analysis_struct.