(Joint Center)Library cauchyreals

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
Require Import bigop ssralg ssrnum ssrint rat poly polydiv polyorder.
Require Import perm matrix mxpoly polyXY binomial bigenough.

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

Set Implicit Arguments.

Delimit Scope creal_scope with CR.

Section poly_extra.

Local Open Scope ring_scope.

Lemma monic_monic_from_neq0 (F : fieldType) (p : {poly F}) :
  (p != 0)%B(lead_coef p) ^-1 *: p \is monic.

GG -- lemmas with ssrnum dependencies cannot go in poly!
Lemma size_derivn (R : realDomainType) (p : {poly R}) n :
  size p^`(n) = (size p - n)%N.

Lemma size_nderivn (R : realDomainType) (p : {poly R}) n :
  size p^`N(n) = (size p - n)%N.

End poly_extra.

Local Notation eval := horner_eval.

Section ordered_extra.

Definition gtr0E := (invr_gt0, exprn_gt0, ltr0n, @ltr01).
Definition ger0E := (invr_ge0, exprn_ge0, ler0n, @ler01).

End ordered_extra.

Section polyorder_extra.

Variable F : realDomainType.

Local Open Scope ring_scope.

Definition poly_bound (p : {poly F}) (a r : F) : F
  := 1 + \sum_(i < size p) `|p`_i| × (`|a| + `|r|) ^+ i.

Lemma poly_boundP p a r x : `|x - a| r
  `|p.[x]| poly_bound p a r.

Lemma poly_bound_gt0 p a r : 0 < poly_bound p a r.

Lemma poly_bound_ge0 p a r : 0 poly_bound p a r.

Definition poly_accr_bound (p : {poly F}) (a r : F) : F
  := (maxr 1 (2%:R × r)) ^+ (size p).-1
  × (1 + \sum_(i < (size p).-1) poly_bound p^`N(i.+1) a r).

Lemma poly_accr_bound1P p a r x y :
  `|x - a| r`|y - a| r
  `|p.[y] - p.[x]| `|y - x| × poly_accr_bound p a r.

Lemma poly_accr_bound_gt0 p a r : 0 < poly_accr_bound p a r.

Lemma poly_accr_bound_ge0 p a r : 0 poly_accr_bound p a r.

Todo : move to polyorder => need char 0
Lemma gdcop_eq0 (p q : {poly F}) :
  (gdcop p q == 0)%B = (q == 0)%B && (p != 0)%B.

End polyorder_extra.

Section polyXY_order_extra.

Variable F : realFieldType.
Local Open Scope ring_scope.

Local Notation "p ^ f" := (map_poly f p) : ring_scope.
Local Notation "'Y" := 'X%:P.

Definition norm_poly2 (p : {poly {poly F}}) := p ^ (map_poly (fun x`|x|)).

Lemma coef_norm_poly2 p i j : (norm_poly2 p)`_i`_j = `|p`_i`_j|.

Lemma size_norm_poly2 p : size (norm_poly2 p) = size p.

End polyXY_order_extra.

Section polyorder_field_extra.

Variable F : realFieldType.

Local Open Scope ring_scope.

Definition poly_accr_bound2 (p : {poly F}) (a r : F) : F
  := (maxr 1 (2%:R × r)) ^+ (size p).-2
  × (1 + \sum_(i < (size p).-2) poly_bound p^`N(i.+2) a r).

Lemma poly_accr_bound2_gt0 p a r : 0 < poly_accr_bound2 p a r.

Lemma poly_accr_bound2_ge0 p a r : 0 poly_accr_bound2 p a r.

Lemma poly_accr_bound2P p (a r x y : F) : (x != y)%B
  `|x - a| r`|y - a| r
  `|(p.[y] - p.[x]) / (y - x) - p^`.[x]|
     `|y - x| × poly_accr_bound2 p a r.

End polyorder_field_extra.

Section monotony.

Variable F : realFieldType.

Local Open Scope ring_scope.

Definition accr_pos p (a r : F) :=
  ({ k | 0 < k & x y, (x != y)%B
    `|x - a| r`|y - a| r(p.[x] - p.[y]) / (x - y) > k }
      × x, `|x - a| rp^`.[x] > 0)%type.

Definition accr_neg p (a r : F) :=
  ({ k | 0 < k & x y, (x != y)%B
    `|x - a| r`|y - a| r(p.[x] - p.[y]) / (x - y) < - k}
      × x, `|x - a| rp^`.[x] < 0)%type.

Definition strong_mono p (a r : F) := (accr_pos p a r + accr_neg p a r)%type.

Lemma accr_pos_incr p a r : accr_pos p a r
   x y, `|x - a| r`|y - a| r(p.[x] p.[y]) = (x y).

Lemma accr_neg_decr p a r : accr_neg p a r
   x y, `|x - a| r`|y - a| r(p.[x] p.[y]) = (y x).

Lemma accr_negN p a r : accr_pos p a raccr_neg (- p) a r.

Lemma accr_posN p a r : accr_neg p a raccr_pos (- p) a r.

Lemma strong_monoN p a r : strong_mono p a rstrong_mono (- p) a r.

Lemma strong_mono_bound p a r : strong_mono p a r
  → {k | 0 < k & x y, `|x - a| r`|y - a| r
    `| x - y | k × `| p.[x] - p.[y] | }.

Definition merge_intervals (ar1 ar2 : F × F) :=
  let l := minr (ar1.1 - ar1.2) (ar2.1 - ar2.2) in
  let u := maxr (ar1.1 + ar1.2) (ar2.1 + ar2.2) in
    ((l + u) / 2%:R, (u - l) / 2%:R).
Local Notation center ar1 ar2 := ((merge_intervals ar1 ar2).1).
Local Notation radius ar1 ar2 := ((merge_intervals ar1 ar2).2).

Lemma split_interval (a1 a2 r1 r2 x : F) :
  0 < r1 → 0 < r2`|a1 - a2| r1 + r2
  (`|x - center (a1, r1) (a2, r2)| radius (a1, r1) (a2, r2))
  = (`|x - a1| r1) || (`|x - a2| r2).

Lemma merge_mono p a1 a2 r1 r2 :
  0 < r1 → 0 < r2
  `|a1 - a2| (r1 + r2)
  strong_mono p a1 r1strong_mono p a2 r2
  strong_mono p (center (a1, r1) (a2, r2)) (radius (a1, r1) (a2, r2)).

End monotony.

Section CauchyReals.

Local Open Scope nat_scope.
Local Open Scope creal_scope.
Local Open Scope ring_scope.

Definition asympt1 (R : numDomainType) (P : RnatProp)
  := {m : Rnat | eps i, 0 < eps → (m eps i)%NP eps i}.

Definition asympt2 (R : numDomainType) (P : RnatnatProp)
  := {m : Rnat | eps i j, 0 < eps → (m eps i)%N → (m eps j)%NP eps i j}.

Notation "{ 'asympt' e : i / P }" := (asympt1 (fun e iP))
  (at level 0, e ident, i ident, format "{ 'asympt' e : i / P }") : type_scope.

Notation "{ 'asympt' e : i j / P }" := (asympt2 (fun e i jP))
  (at level 0, e ident, i ident, j ident, format "{ 'asympt' e : i j / P }") : type_scope.

Lemma asympt1modP (R : numDomainType) P (a : asympt1 P) e i :
  0 < e :> R → (projT1 a e i)%NP e i.

Lemma asympt2modP (R : numDomainType) P (a : asympt2 P) e i j :
  0 < e :> R → (projT1 a e i)%N → (projT1 a e j)%NP e i j.

Variable F : realFieldType.

Lemma asympt_mulLR (k : F) (hk : 0 < k) (P : F -> nat -> Prop) : {asympt e : i / P e i} -> {asympt e : i / P (e * k) i}. Proof. case=> m hm; exists (fun e => m (e * k))=> e i he hi. by apply: hm=> //; rewrite -ltr_pdivr_mulr // mul0r. Qed.
Lemma asympt_mulRL (k : F) (hk : 0 < k) (P : F -> nat -> Prop) : {asympt e : i / P (e * k) i} -> {asympt e : i / P e i}. Proof. case=> m hm; exists (fun e => m (e / k))=> e i he hi. rewrite - [e](@mulfVK _ k) ?gtr_eqF //. by apply: hm=> //; rewrite -ltr_pdivr_mulr ?invr_gt0 // mul0r. Qed.

Lemma asymptP (P1 : FnatProp) (P2 : FnatProp) :
  ( e i, 0 < eP1 e iP2 e i) →
  {asympt e : i / P1 e i}{asympt e : i / P2 e i}.

Lemma asympt2_mulLR (k : F) (hk : 0 < k) (P : F -> nat -> nat -> Prop) : {asympt e : i j / P e i j} -> {asympt e : i j / P (e * k) i j}. Proof. case=> m hm; exists (fun e => m (e * k))=> e i j he hi hj. by apply: hm=> //; rewrite -ltr_pdivr_mulr // mul0r. Qed.
Lemma asympt2_mulRL (k : F) (hk : 0 < k) (P : F -> nat -> nat -> Prop) : {asympt e : i j / P (e * k) i j} -> {asympt e : i j / P e i j}. Proof. case=> m hm; exists (fun e => m (e / k))=> e i j he hi hj. rewrite - [e](@mulfVK _ k) ?gtr_eqF //. by apply: hm=> //; rewrite -ltr_pdivr_mulr ?invr_gt0 // mul0r. Qed.
Lemma asympt2P (P1 : F -> nat -> nat -> Prop) (P2 : F -> nat -> nat -> Prop) : (forall e i j, 0 < e -> P1 e i j -> P2 e i j) -> {asympt e : i j / P1 e i j} -> {asympt e : i j / P2 e i j}. Proof. move=> hP; case=> m hm; exists m=> e i j he mei mej. by apply: hP=> //; apply: hm. Qed.

Lemma splitf (n : nat) (e : F) : e = iterop n +%R (e / n%:R) e.

Lemma splitD (x y e : F) : x < e / 2%:Ry < e / 2%:Rx + y < e.

Lemma divrn_gt0 (e : F) (n : nat) : 0 < e → (0 < n)%N → 0 < e / n%:R.

Lemma split_norm_add (x y e : F) :
  `|x| < e / 2%:R`|y| < e / 2%:R`|x + y| < e.

Lemma split_norm_sub (x y e : F) :
  `|x| < e / 2%:R`|y| < e / 2%:R`|x - y| < e.

Lemma split_dist_add (z x y e : F) :
  `|x - z| < e / 2%:R`|z - y| < e / 2%:R`|x - y| < e.

Definition creal_axiom (x : natF) := {asympt e : i j / `|x i - x j| < e}.

CoInductive creal := CReal {cauchyseq :> natF; _ : creal_axiom cauchyseq}.

Lemma crealP (x : creal) : {asympt e : i j / `|x i - x j| < e}.

Definition cauchymod :=
  nosimpl (fun (x : creal) ⇒ let: CReal _ m := x in projT1 m).

Lemma cauchymodP (x : creal) eps i j : 0 < eps
  (cauchymod x eps i)%N → (cauchymod x eps j)%N`|x i - x j| < eps.

Definition neq_creal (x y : creal) : Prop :=
   eps, (0 < eps) &&
    (eps × 3%:R `|x (cauchymod x eps) - y (cauchymod y eps)|).
Notation "!=%CR" := neq_creal : creal_scope.
Notation "x != y" := (neq_creal x y) : creal_scope.

Definition eq_creal x y := (¬ (x != y)%CR).
Notation "x == y" := (eq_creal x y) : creal_scope.

Lemma ltr_distl_creal (e : F) (i : nat) (x : creal) (j : nat) (a b : F) :
  0 < e → (cauchymod x e i)%N → (cauchymod x e j)%N
  `| x i - a | b - e`| x j - a | < b.

Lemma ltr_distr_creal (e : F) (i : nat) (x : creal) (j : nat) (a b : F) :
  0 < e → (cauchymod x e i)%N → (cauchymod x e j)%N
  a + e `| x i - b |a < `| x j - b |.

Lemma asympt_neq (x y : creal) : x != y -> {e | 0 < e & forall i, (cauchymod x e <= i)%N -> (cauchymod y e <= i)%N -> `|x i - y i| >= e}. Proof. case/sigW=> e /andP[e_gt0 hxy]. exists e=> // i hi hj; move: hxy; rewrite !lerNgt; apply: contra=> hxy. rewrite !mulrDr !mulr1 distrC (@ltr_distl_creal i) //. by rewrite distrC ltrW // (@ltr_distl_creal i) // ltrW. Qed.

Definition lbound (x y : creal) (neq_xy : x != y) : F :=
  projT1 (sigW neq_xy).

Lemma lboundP (x y : creal) (neq_xy : x != y) i :
  (cauchymod x (lbound neq_xy) i)%N
  (cauchymod y (lbound neq_xy) i)%Nlbound neq_xy `|x i - y i|.

Notation lbound_of p := (@lboundP _ _ p _ _ _).

Lemma lbound_gt0 (x y : creal) (neq_xy : x != y) : lbound neq_xy > 0.

Definition lbound_ge0 x y neq_xy := (ltrW (@lbound_gt0 x y neq_xy)).

Lemma cst_crealP (x : F) : creal_axiom (fun _x).
Definition cst_creal (x : F) := CReal (cst_crealP x).
Notation "x %:CR" := (cst_creal x)
  (at level 2, left associativity, format "x %:CR") : creal_scope.
Notation "0" := (0 %:CR) : creal_scope.

Lemma lbound0P (x : creal) (x_neq0 : x != 0) i :
  (cauchymod x (lbound x_neq0) i)%N
  (cauchymod 0%CR (lbound x_neq0) i)%Nlbound x_neq0 `|x i|.

Notation lbound0_of p := (@lbound0P _ p _ _ _).

Lemma neq_crealP e i j (e_gt0 : 0 < e) (x y : creal) :
  (cauchymod x (e / 5%:R) i)%N → (cauchymod y (e / 5%:R) j)%N
  e `|x i - y j|x != y.

Lemma eq_crealP (x y : creal) : {asympt e : i / `|x i - y i| < e}
  (x == y)%CR.

Lemma eq0_crealP (x : creal) : {asympt e : i / `|x i| < e}x == 0.

Lemma asympt_eq (x y : creal) (eq_xy : x == y) :
  {asympt e : i / `|x i - y i| < e}.

Lemma asympt_eq0 (x : creal) : x == 0 → {asympt e : i / `|x i| < e}.

Definition eq_mod (x y : creal) (eq_xy : x == y) := projT1 (asympt_eq eq_xy).
Lemma eq_modP (x y : creal) (eq_xy : x == y) eps i : 0 < eps
                (eq_mod eq_xy eps i)%N`|x i - y i| < eps.
Lemma eq0_modP (x : creal) (x_eq0 : x == 0) eps i : 0 < eps
                (eq_mod x_eq0 eps i)%N`|x i| < eps.

Lemma eq_creal_refl x : x == x.
Hint Resolve eq_creal_refl.

Lemma neq_creal_sym x y : x != yy != x.

Lemma eq_creal_sym x y : x == yy == x.

Lemma eq_creal_trans x y z : x == yy == zx == z.

Lemma creal_neq_always (x y : creal) i (neq_xy : x != y) :
  (cauchymod x (lbound neq_xy) i)%N
  (cauchymod y (lbound neq_xy) i)%N → (x i != y i)%B.

Definition creal_neq0_always (x : creal) := @creal_neq_always x 0.

Definition lt_creal (x y : creal) : Prop :=
   eps, (0 < eps) &&
    (x (cauchymod x eps) + eps × 3%:R y (cauchymod y eps)).
Notation "<%CR" := lt_creal : creal_scope.
Notation "x < y" := (lt_creal x y) : creal_scope.

Definition le_creal (x y : creal) : Prop := ¬ (y < x)%CR.
Notation "<=%CR" := le_creal : creal_scope.
Notation "x <= y" := (le_creal x y) : creal_scope.

Lemma ltr_creal (e : F) (i : nat) (x : creal) (j : nat) (a : F) :
  0 < e → (cauchymod x e i)%N → (cauchymod x e j)%N
  x i a - ex j < a.

Lemma gtr_creal (e : F) (i : nat) (x : creal) (j : nat) (a : F) :
  0 < e → (cauchymod x e i)%N → (cauchymod x e j)%N
  a + e x ia < x j.

Definition diff (x y : creal) (lt_xy : (x < y)%CR) : F := projT1 (sigW lt_xy).

Lemma diff_gt0 (x y : creal) (lt_xy : (x < y)%CR) : diff lt_xy > 0.

Definition diff_ge0 x y lt_xy := (ltrW (@diff_gt0 x y lt_xy)).

Lemma diffP (x y : creal) (lt_xy : (x < y)%CR) i :
  (cauchymod x (diff lt_xy) i)%N
  (cauchymod y (diff lt_xy) i)%Nx i + diff lt_xy y i.

Notation diff_of p := (@diffP _ _ p _ _ _).

Lemma diff0P (x : creal) (x_gt0 : (0 < x)%CR) i :
  (cauchymod x (diff x_gt0) i)%N
  (cauchymod 0%CR (diff x_gt0) i)%Ndiff x_gt0 x i.

Notation diff0_of p := (@diff0P _ p _ _ _).

Lemma lt_crealP e i j (e_gt0 : 0 < e) (x y : creal) :
  (cauchymod x (e / 5%:R) i)%N → (cauchymod y (e / 5%:R) j)%N
  x i + e y j → (x < y)%CR.

Lemma le_crealP i (x y : creal) :
  ( j, (i j)%Nx j y j) → (x y)%CR.

Lemma le_creal_refl (x : creal) : (x x)%CR.
Hint Resolve le_creal_refl.

Lemma lt_neq_creal (x y : creal) : (x < y)%CRx != y.

Lemma creal_lt_always (x y : creal) i (lt_xy : (x < y)%CR) :
  (cauchymod x (diff lt_xy) i)%N
  (cauchymod y (diff lt_xy) i)%Nx i < y i.

Definition creal_gt0_always := @creal_lt_always 0.

Lemma eq_le_creal (x y : creal) : x == y → (x y)%CR.

Lemma asympt_le (x y : creal) (le_xy : (x y)%CR) :
  {asympt e : i / x i < y i + e}.

Lemma asympt_ge0 (x : creal) : (0 x)%CR{asympt e : i / - e < x i}.

Definition le_mod (x y : creal) (le_xy : (x y)%CR) := projT1 (asympt_le le_xy).

Lemma le_modP (x y : creal) (le_xy : (x y)%CR) eps i : 0 < eps
                (le_mod le_xy eps i)%Nx i < y i + eps.

Lemma ge0_modP (x : creal) (x_ge0 : (0 x)%CR) eps i : 0 < eps
                (le_mod x_ge0 eps i)%N- eps < x i.

Lemma opp_crealP (x : creal) : creal_axiom (fun i- x i).
Definition opp_creal (x : creal) := CReal (opp_crealP x).
Notation "-%CR" := opp_creal : creal_scope.
Notation "- x" := (opp_creal x) : creal_scope.

Lemma add_crealP (x y : creal) : creal_axiom (fun ix i + y i).
Definition add_creal (x y : creal) := CReal (add_crealP x y).
Notation "+%CR" := add_creal : creal_scope.
Notation "x + y" := (add_creal x y) : creal_scope.
Notation "x - y" := (x + - y)%CR : creal_scope.

Lemma ubound_subproof (x : creal) : {b : F | b > 0 & i, `|x i| b}.

Definition ubound (x : creal) :=
  nosimpl (let: exist2 b _ _ := ubound_subproof x in b).

Lemma uboundP (x : creal) i : `|x i| ubound x.

Lemma ubound_gt0 x : 0 < ubound x.

Definition ubound_ge0 x := (ltrW (ubound_gt0 x)).

Lemma mul_crealP (x y : creal) : creal_axiom (fun ix i × y i).
Definition mul_creal (x y : creal) := CReal (mul_crealP x y).
Notation "*%CR" := mul_creal : creal_scope.
Notation "x * y" := (mul_creal x y) : creal_scope.

Lemma inv_crealP (x : creal) (x_neq0 : x != 0) : creal_axiom (fun i(x i)^-1).
Definition inv_creal (x : creal) (x_neq0 : x != 0) := CReal (inv_crealP x_neq0).
Notation "x_neq0 ^-1" := (inv_creal x_neq0) : creal_scope.
Notation "x / y_neq0" := (x × (y_neq0 ^-1))%CR : creal_scope.

Lemma norm_crealP (x : creal) : creal_axiom (fun i`|x i|).
Definition norm_creal x := CReal (norm_crealP x).
Local Notation "`| x |" := (norm_creal x) : creal_scope.

Lemma horner_crealP (p : {poly F}) (x : creal) :
  creal_axiom (fun ip.[x i]).
Definition horner_creal (p : {poly F}) (x : creal) := CReal (horner_crealP p x).
Notation "p .[ x ]" := (horner_creal p x) : creal_scope.

Lemma neq_creal_horner p (x y : creal) : p.[x] != p.[y]x != y.

Lemma eq_creal_horner p (x y : creal) : x == yp.[x] == p.[y].

Import Setoid Relation_Definitions.

Add Relation creal eq_creal
  reflexivity proved by eq_creal_refl
  symmetry proved by eq_creal_sym
  transitivity proved by eq_creal_trans
as eq_creal_rel.
Global
Add Morphism add_creal with
  signature eq_creal ==> eq_creal ==> eq_creal as add_creal_morph.
Global
Add Morphism opp_creal with
  signature eq_creal ==> eq_creal as opp_creal_morph.
Global
Add Morphism mul_creal with
  signature eq_creal ==> eq_creal ==> eq_creal as mul_creal_morph.
Global
Lemma eq_creal_inv (x y : creal) (x_neq0 : x != 0) (y_neq0 : y != 0) :
  (x == y) → (x_neq0^-1 == y_neq0^-1).

Add Morphism horner_creal with
  signature (@eq _) ==> eq_creal ==> eq_creal as horner_creal_morph.
Global
Add Morphism lt_creal with
  signature eq_creal ==> eq_creal ==> iff as lt_creal_morph.
Global
Add Morphism le_creal with
  signature eq_creal ==> eq_creal ==> iff as le_creal_morph.
Global
Add Morphism norm_creal
 with signature eq_creal ==> eq_creal as norm_creal_morph.
Global
Lemma neq_creal_ltVgt (x y : creal) : x != y{(x < y)%CR} + {(y < x)%CR}.

Lemma lt_creal_neq (x y : creal) : (x < yx != y)%CR.

Lemma gt_creal_neq (x y : creal) : (y < xx != y)%CR.

Lemma lt_creal_trans (x y z : creal) : (x < yy < zx < z)%CR.

Lemma lt_crealW (x y : creal) : (x < y)%CR → (x y)%CR.

Add Morphism neq_creal with
  signature eq_creal ==> eq_creal ==> iff as neq_creal_morph.
Global
Local Notation m0 := (fun (_ : F) ⇒ 0%N).

Lemma add_0creal x : 0 + x == x.

Lemma add_creal0 x : x + 0 == x.

Lemma mul_creal0 x : x × 0 == 0.

Lemma mul_0creal x : 0 × x == 0.

Lemma mul_creal1 x : x × 1%:CR == x.

Lemma mul_1creal x : 1%:CR × x == x.

Lemma opp_creal0 : - 0 == 0.

Lemma horner_crealX (x : creal) : 'X.[x] == x.

Lemma horner_crealM (p q : {poly F}) (x : creal) :
  ((p × q).[x] == p.[x] × q.[x])%CR.

Lemma neq_creal_cst x y : reflect (cst_creal x != cst_creal y) (x != y).

Lemma eq_creal_cst x y : reflect (cst_creal x == cst_creal y) (x == y).

Lemma lt_creal_cst x y : reflect (cst_creal x < cst_creal y)%CR (x < y).

Lemma le_creal_cst x y : reflect (cst_creal x cst_creal y)%CR (x y).

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

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

Lemma poly_mul_creal_eq0_coprime p q x :
  coprimep p q
  p.[x] × q.[x] == 0 → {p.[x] == 0} + {q.[x] == 0}.

Lemma dvdp_creal_eq0 p q x : p %| qp.[x] == 0 → q.[x] == 0.

Lemma root_poly_expn_creal p k x : (0 < k)%N
  → (p ^+ k).[x] == 0 → p.[x] == 0.

Lemma horner_cst_creal c x : c%:P.[x] == c%:CR.

Lemma horner_creal_cst (p : {poly F}) (x : F) : p.[x%:CR] == p.[x]%:CR.

Lemma poly_mul_creal_eq0 p q x :
  p.[x] × q.[x] == 0 → {p.[x] == 0} + {q.[x] == 0}.

Lemma coprimep_root (p q : {poly F}) x :
  coprimep p qp.[x] == 0 → q.[x] != 0.

Lemma deriv_neq0_mono (p : {poly F}) (x : creal) : p^`.[x] != 0 →
  { r : F & 0 < r &
    { i : nat & (cauchymod x r i)%N & (strong_mono p (x i) r)} }.

Lemma smaller_factor (p q : {poly F}) x :
  p \is monicp.[x] == 0 →
  ~~(p %| q)~~ coprimep p q
  {r : {poly F} | (size r < size p)%N && (r \is monic) & r.[x] == 0}.

Lemma root_cst_creal (x : F) : ('X - x%:P).[cst_creal x] == 0.

Lemma has_root_creal_size_gt1 (x : creal) (p : {poly F}) :
  (p != 0)%Bp.[x] == 0 → (1 < size p)%N.

Definition bound_poly_bound (z : creal) (q : {poly {poly F}}) (a r : F) i :=
  (1 + \sum_(j < sizeY q)
    `|(norm_poly2 q).[(ubound z)%:P]^`N(i.+1)`_j| × (`|a| + `|r|) ^+ j).

Lemma bound_poly_boundP (z : creal) i (q : {poly {poly F}}) (a r : F) j :
  poly_bound q.[(z i)%:P]^`N(j.+1) a r bound_poly_bound z q a r j.

Lemma bound_poly_bound_ge0 z q a r i : 0 bound_poly_bound z q a r i.

Definition bound_poly_accr_bound (z : creal) (q : {poly {poly F}}) (a r : F) :=
   maxr 1 (2%:R × r) ^+ (sizeY q).-1 ×
   (1 + \sum_(i < (sizeY q).-1) bound_poly_bound z q a r i).

Lemma bound_poly_accr_boundP (z : creal) i (q : {poly {poly F}}) (a r : F) :
  poly_accr_bound q.[(z i)%:P] a r bound_poly_accr_bound z q a r.

Lemma bound_poly_accr_bound_gt0 (z : creal) (q : {poly {poly F}}) (a r : F) :
  0 < bound_poly_accr_bound z q a r.

Lemma horner2_crealP (p : {poly {poly F}}) (x y : creal) :
  creal_axiom (fun ip.[x i, y i]).

Definition horner2_creal (p : {poly {poly F}}) (x y : creal) :=
  CReal (horner2_crealP p x y).
Notation "p .[ x , y ]" := (horner2_creal p x y)
  (at level 2, left associativity) : creal_scope.

Lemma root_monic_from_neq0 (p : {poly F}) (x : creal) :
  p.[x] == 0 → ((lead_coef p) ^-1 *: p).[x] == 0.

Lemma root_sub_annihilant_creal (x y : creal) (p q : {poly F}) :
  (p != 0)%B → (q != 0)%Bp.[x] == 0 → q.[y] == 0 →
  (sub_annihilant p q).[x - y] == 0.

Lemma root_div_annihilant_creal (x y : creal) (p q : {poly F}) (y_neq0 : y != 0) :
  (p != 0)%B → (q != 0)%Bp.[x] == 0 → q.[y] == 0 →
  (div_annihilant p q).[(x / y_neq0)%CR] == 0.

Definition exp_creal x n := (iterop n *%CR x 1%:CR).
Notation "x ^+ n" := (exp_creal x n) : creal_scope.

Add Morphism exp_creal with
  signature eq_creal ==> (@eq _) ==> eq_creal as exp_creal_morph.
Global
Lemma horner_coef_creal p x :
   p.[x] == \big[+%CR/0%:CR]_(i < size p) ((p`_i)%:CR × (x ^+ i))%CR.

End CauchyReals.

Notation "x == y" := (eq_creal x y) : creal_scope.
Notation "!=%CR" := neq_creal : creal_scope.
Notation "x != y" := (neq_creal x y) : creal_scope.

Notation "x %:CR" := (cst_creal x)
  (at level 2, left associativity, format "x %:CR") : creal_scope.
Notation "0" := (0 %:CR)%CR : creal_scope.

Notation "<%CR" := lt_creal : creal_scope.
Notation "x < y" := (lt_creal x y) : creal_scope.

Notation "<=%CR" := le_creal : creal_scope.
Notation "x <= y" := (le_creal x y) : creal_scope.

Notation "-%CR" := opp_creal : creal_scope.
Notation "- x" := (opp_creal x) : creal_scope.

Notation "+%CR" := add_creal : creal_scope.
Notation "x + y" := (add_creal x y) : creal_scope.
Notation "x - y" := (x + - y)%CR : creal_scope.

Notation "*%CR" := mul_creal : creal_scope.
Notation "x * y" := (mul_creal x y) : creal_scope.

Notation "x_neq0 ^-1" := (inv_creal x_neq0) : creal_scope.
Notation "x / y_neq0" := (x × (y_neq0 ^-1))%CR : creal_scope.
Notation "p .[ x ]" := (horner_creal p x) : creal_scope.
Notation "p .[ x , y ]" := (horner2_creal p x y)
  (at level 2, left associativity) : creal_scope.
Notation "x ^+ n" := (exp_creal x n) : creal_scope.

Notation "`| x |" := (norm_creal x) : creal_scope.

Hint Resolve eq_creal_refl.
Hint Resolve le_creal_refl.

Notation lbound_of p := (@lboundP _ _ _ p _ _ _).
Notation lbound0_of p := (@lbound0P _ _ p _ _ _).
Notation diff_of p := (@diffP _ _ _ p _ _ _).
Notation diff0_of p := (@diff0P _ _ p _ _ _).

Notation "{ 'asympt' e : i / P }" := (asympt1 (fun e iP))
  (at level 0, e ident, i ident, format "{ 'asympt' e : i / P }") : type_scope.
Notation "{ 'asympt' e : i j / P }" := (asympt2 (fun e i jP))
  (at level 0, e ident, i ident, j ident, format "{ 'asympt' e : i j / P }") : type_scope.