CoRN.reals.NRootIR

Require Export OddPolyRootIR.

Roots of Real Numbers

Section NRoot.

Existence of roots

Let n be a natural number and c a nonnegative real. p is the auxiliary polynomial _X_[^]n[-] (_C_ c).

Variable n : nat.
Hypothesis n_pos : 0 < n.
Variable c : IR.
Hypothesis c_nonneg : [0] [<=] c.

Lemma CnrootIR : {x : IR | [0] [<=] x | x[^]n [=] c }.
Proof.
intros.
cut (monic n p). intro.
  elim (Ccpoly_pos' _ p [0] n); auto.
  intro X. intros H0 H1.
  cut {x : IR | [0] [<=] x ∧ x [<=] X ∧ p ! x [=] [0]}. intro H2.
   elim H2. clear H2. intro. intro H2.
   elim H2. clear H2. intros H2 H3. elim H3. clear H3. intros.
   ∃ x. auto.
    apply cg_inv_unique_2.
   astepl (_X_ ! x[^]n [-] (_C_ c ) ! x).
   astepl ((_X_[^]n ) ! x[-] (_C_ c ) ! x).
   Step_final (_X_[^]n [-]_C_ c ) ! x.
  apply Civt_poly; auto.
   apply monic_apzero with n; auto.
  unfold p in |- ×.
  astepl ((_X_[^]n ) ! [0][-] (_C_ c ) ! [0]).
  astepl (_X_ ! [0][^]n [-]c).
  astepl ([0][^]n [-]c).
  astepl ([0][-]c).
  astepl ( [--]c).
  astepr ( [--]ZeroR). apply inv_resp_leEq. auto.
  unfold p in |- ×.
apply monic_minus with 0.
   apply degree_le_c_.
  pattern n at 1 in |- ×. replace n with (1 × n).
  apply monic_nexp.
   apply monic_x_.
  auto with arith.
auto.
Qed.

End NRoot.

We define the root of order n for any nonnegative real number and prove its main properties:

(sqrt(n) x)^n =x;
0≤sqrt(n)x;
if [0] [<] x then 0<sqrt(n)x;
sqrt(n) x^n =x;
the nth root is monotonous;
in particular, if x [<] [1] then sqrt(n) x<1.

(nroot ??) will be written as NRoot.

Section Nth_Root.

Lemma nroot : ∀ x k, [0] [<=] x → 0 < k → {y : IR | [0] [<=] y | y[^]k [=] x }.
Proof.
intros.
elim (CnrootIR k H0 x H). intro y. intros.
∃ y; auto.
Qed.

Definition NRoot x n Hx Hn : IR := proj1_sig2T _ _ _ (nroot x n Hx Hn).

Lemma NRoot_power : ∀ x k Hx Hk, NRoot x k Hx Hk [^]k [=] x.
Proof.
intros.
unfold NRoot in |- ×.
apply proj2b_sig2T.
Qed.

Hint Resolve NRoot_power: algebra.

Lemma NRoot_nonneg : ∀ x k Hx Hk, [0] [<=] NRoot x k Hx Hk.
Proof.
intros.
unfold NRoot in |- ×.
apply proj2a_sig2T.
Qed.

Lemma NRoot_pos : ∀ x Hx k Hk, [0] [<] x → [0] [<] NRoot x k Hx Hk.
Proof.
intros. rename X into H.
cut ([0] [<=] NRoot x k Hx Hk); intros.
  cut (NRoot x k Hx Hk [<] [0] or [0] [<] NRoot x k Hx Hk). intros H1.
   elim H1; clear H1; intro H1.
    rewrite → leEq_def in H0; elim (H0 H1).
   auto.
  apply ap_imp_less.
  apply un_op_strext_unfolded with (nexp_op (R:=IR) k).
  astepl x; astepr ZeroR.
  apply pos_ap_zero; auto.
apply NRoot_nonneg.
Qed.

Lemma NRoot_power' : ∀ x k Hx' Hk, [0] [<=] x → NRoot (x [^]k) k Hx' Hk [=] x.
Proof.
intros.
apply root_unique with k; auto.
  apply NRoot_nonneg.
apply NRoot_power.
Qed.

Lemma NRoot_pres_less : ∀ x Hx y Hy k Hk, x [<] y → NRoot x k Hx Hk [<] NRoot y k Hy Hk.
Proof.
intros.
apply power_cancel_less with k.
  apply NRoot_nonneg.
eapply less_wdl.
  2: apply eq_symmetric_unfolded; apply NRoot_power.
eapply less_wdr.
  2: apply eq_symmetric_unfolded; apply NRoot_power.
auto.
Qed.

Lemma NRoot_less_one : ∀ x Hx k Hk, x [<] [1] → NRoot x k Hx Hk [<] [1].
Proof.
intros.
apply power_cancel_less with k.
  apply less_leEq; apply pos_one.
eapply less_wdl.
  2: apply eq_symmetric_unfolded; apply NRoot_power.
astepr OneR.
assumption.
Qed.

Lemma NRoot_cancel : ∀ x Hx y Hy k Hk, NRoot x k Hx Hk [=] NRoot y k Hy Hk → x [=] y.
Proof.
intros.
apply eq_transitive_unfolded with (NRoot x k Hx Hk[^]k).
  apply eq_symmetric_unfolded; apply NRoot_power.
apply eq_transitive_unfolded with (NRoot y k Hy Hk[^]k).
  2: apply NRoot_power.
apply nexp_wd; algebra.
Qed.

Let x,y be nonnegative real numbers.

Variables x y : IR.
Hypothesis Hx : [0] [<=] x.
Hypothesis Hy : [0] [<=] y.

Lemma NRoot_wd : ∀ k Hk Hk', x [=] y → NRoot x k Hx Hk [=] NRoot y k Hy Hk'.
Proof.
intros.
apply root_unique with k; auto.
   apply NRoot_nonneg.
  apply NRoot_nonneg.
eapply eq_transitive_unfolded.
  eapply eq_transitive_unfolded.
   2: apply H.
  apply NRoot_power.
apply eq_symmetric_unfolded; apply NRoot_power.
Qed.

Lemma NRoot_unique : ∀ k Hk, [0] [<] x → x [^]k [=] y → x [=] NRoot y k Hy Hk.
Proof.
intros. rename H into H0.
apply root_unique with k; auto.
  apply NRoot_nonneg.
eapply eq_transitive_unfolded.
  apply H0.
apply eq_symmetric_unfolded; apply NRoot_power.
Qed.

End Nth_Root.

Implicit Arguments NRoot [x n].

Hint Resolve NRoot_power NRoot_power': algebra.

Lemma NRoot_resp_leEq : ∀ x y xpos ypos k kpos,
x [<=] y → NRoot (x:=x) (n:=k) xpos kpos [<=] NRoot (x:=y) (n:=k) ypos kpos.
Proof.
intros.
rewrite → leEq_def; intro H0.
assert (NRoot ypos kpos[^]k [<=] NRoot xpos kpos[^]k).
  apply power_resp_leEq.
   apply NRoot_nonneg.
  apply less_leEq; auto.
assert (x [=] y).
  apply leEq_imp_eq; auto.
  eapply leEq_wdl.
   eapply leEq_wdr.
    eexact H1.
   algebra.
  algebra.
clear H H1.
generalize (NRoot_wd _ _ xpos ypos k kpos kpos H2).
intro.
apply (less_irreflexive_unfolded _ (NRoot ypos kpos)).
astepr (NRoot xpos kpos).
auto.
Qed.

Lemma NRoot_cancel_less : ∀ x (Hx:[0][<=]x) y (Hy:[0][<=]y) k (Hk Hk':0<k), NRoot Hx Hk [<] NRoot Hy Hk' → x [<] y.
Proof.
intros x Hx y Hy k Hk Hk' H.
astepl (NRoot Hx Hk[^]k).
astepr (NRoot Hy Hk'[^]k).
apply nexp_resp_less.
   auto with ×.
  apply NRoot_nonneg.
assumption.
Qed.

Lemma NRoot_str_ext : ∀ k (Hk Hk':0 < k) x y (Hx:[0][<=]x) (Hy:[0][<=]y), NRoot Hx Hk [#] NRoot Hy Hk' → x [#]y.
Proof.
intros k Hk Hk' x y Hx Hy H0.
destruct (ap_imp_less _ _ _ H0) as [H1|H1].
  apply less_imp_ap.
  refine (NRoot_cancel_less _ _ _ _ _ _ _ H1).
apply Greater_imp_ap.
refine (NRoot_cancel_less _ _ _ _ _ _ _ H1).
Qed.

Section Square_root.

Square root

Definition sqrt x xpos : IR := NRoot (x:=x) (n:=2) xpos (lt_O_Sn 1).

Lemma sqrt_sqr : ∀ x xpos, sqrt x xpos [^]2 [=] x.
Proof.
intros.
unfold sqrt in |- ×.
apply NRoot_power.
Qed.

Hint Resolve sqrt_sqr: algebra.

Lemma sqrt_nonneg : ∀ x xpos, [0] [<=] sqrt x xpos.
Proof.
intros.
unfold sqrt in |- ×.
apply NRoot_nonneg.
Qed.

Lemma sqrt_wd : ∀ x y xpos ypos, x [=] y → sqrt x xpos [=] sqrt y ypos.
Proof.
intros.
unfold sqrt in |- ×.
apply NRoot_wd.
auto.
Qed.

Hint Resolve sqrt_wd: algebra_c.

Lemma sqrt_to_nonneg : ∀ x, [0] [<=] x → ∀ x2pos, sqrt (x [^]2) x2pos [=] x.
Proof.
intros.
apply root_unique with 2.
    apply sqrt_nonneg. auto. auto.
   Step_final (x[^]2).
Qed.

Lemma sqrt_to_nonpos : ∀ x, x [<=] [0] → ∀ x2pos, sqrt (x [^]2) x2pos [=] [--]x.
Proof.
intros.
apply root_unique with 2.
    apply sqrt_nonneg.
   astepl ( [--]ZeroR). apply inv_resp_leEq. auto.
   auto.
astepl (x[^]2). rational.
Qed.

Lemma sqrt_mult : ∀ x y xpos ypos xypos, sqrt (x [*]y) xypos [=] sqrt x xpos [*]sqrt y ypos.
Proof.
intros.
apply root_unique with 2.
    apply sqrt_nonneg.
   apply mult_resp_nonneg; apply sqrt_nonneg.
  auto.
astepl (x[*]y).
astepl (sqrt x xpos[^]2[*]sqrt y ypos[^]2).
rational.
Qed.

Hint Resolve sqrt_mult: algebra.

Lemma sqrt_mult_wd : ∀ x y z xpos ypos zpos,
z [=] x [*]y → sqrt z zpos [=] sqrt x xpos [*]sqrt y ypos.
Proof.
intros.
cut ([0] [<=] x[*]y). intro.
  Step_final (sqrt (x[*]y) H0).
apply mult_resp_nonneg; auto.
Qed.

Lemma sqrt_less : ∀ x y ypos, x [^]2 [<] y → x [<] sqrt y ypos.
Proof.
intros.
apply power_cancel_less with 2.
  apply sqrt_nonneg.
astepr y. auto.
Qed.

Lemma sqrt_less' : ∀ x y ypos, x [^]2 [<] y → [--]x [<] sqrt y ypos.
Proof.
intros.
apply power_cancel_less with 2.
  apply sqrt_nonneg.
rstepl (x[^]2). astepr y. auto.
Qed.

Lemma sqrt_resp_leEq : ∀ x y xpos ypos, x [<=] y → sqrt x xpos [<=] sqrt y ypos.
Proof.
intros.
unfold sqrt in |- ×.
apply NRoot_resp_leEq.
auto.
Qed.

Lemma sqrt_resp_less : ∀ x y xpos ypos, x [<] y → sqrt x xpos [<] sqrt y ypos.
Proof.
intros.
unfold sqrt in |- ×.
apply NRoot_pres_less.
auto.
Qed.

End Square_root.

Hint Resolve sqrt_wd: algebra_c.
Hint Resolve sqrt_sqr sqrt_mult: algebra.

Section Absolute_Props.

More on absolute value

With the help of square roots, we can prove some more properties of absolute values in IR.

Lemma AbsIR_sqrt_sqr : ∀ x x2pos, AbsIR x [=] sqrt (x [^]2) x2pos.
Proof.
intros x xxpos. unfold AbsIR in |- ×. simpl in |- ×. unfold ABSIR in |- ×.
apply equiv_imp_eq_max; intros.
   apply power_cancel_leEq with 2.
     auto.
    apply mult_cancel_leEq with (Two:IR). apply pos_two.
     rstepl (x[+][--]x).
    rstepr (y[+]y).
    apply plus_resp_leEq_both; auto.
   astepl ([1][*]x[*]x).
   rstepl (x[^]2[+][0]).
   apply shift_plus_leEq'.
   rstepr ((y[-]x) [*] (y[-][--]x)).
   apply mult_resp_nonneg.
    apply shift_zero_leEq_minus. auto.
    apply shift_zero_leEq_minus. auto.
   apply leEq_transitive with (sqrt (x[^]2) xxpos).
   apply power_cancel_leEq with 2. auto.
     apply sqrt_nonneg.
   astepr (x[^]2).
   apply leEq_reflexive.
  auto.
apply leEq_transitive with (sqrt (x[^]2) xxpos).
  apply power_cancel_leEq with 2. auto.
    apply sqrt_nonneg.
  astepr (x[^]2).
  rstepl (x[^]2).
  apply leEq_reflexive.
auto.
Qed.

Hint Resolve AbsIR_sqrt_sqr: algebra.

Lemma AbsIR_resp_mult : ∀ x y, AbsIR (x [*]y) [=] AbsIR x [*]AbsIR y.
Proof.
intros.
astepl (sqrt ((x[*]y) [^]2) (sqr_nonneg _ (x[*]y))).
cut ([0] [<=] x[^]2[*]y[^]2). intro.
  astepl (sqrt (x[^]2[*]y[^]2) H).
  Step_final (sqrt (x[^]2) (sqr_nonneg _ x) [*]sqrt (y[^]2) (sqr_nonneg _ y)).
apply mult_resp_nonneg; apply sqr_nonneg.
Qed.

Lemma AbsIR_mult_pos : ∀ x y, [0] [<=] y → AbsIR (x [*]y) [=] AbsIR x [*]y.
Proof.
intros.
apply eq_transitive_unfolded with (AbsIR x[*]AbsIR y).
  apply AbsIR_resp_mult.
apply bin_op_wd_unfolded.
  algebra.
unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- ×.
apply eq_transitive_unfolded with (Max [--]y y).
  apply Max_comm.
apply leEq_imp_Max_is_rht.
apply leEq_transitive with ZeroR.
  astepr ( [--]ZeroR).
  apply inv_resp_leEq; assumption.
assumption.
Qed.

Lemma AbsIR_mult_pos' : ∀ x y, [0] [<=] x → AbsIR (x [*]y) [=] x [*]AbsIR y.
Proof.
intros.
astepl (AbsIR (y[*]x)).
eapply eq_transitive_unfolded.
  apply AbsIR_mult_pos; auto.
algebra.
Qed.

Lemma AbsIR_nexp : ∀ x n, AbsIR (nexp _ n x) [=] nexp _ n (AbsIR x).
Proof.
intros.
induction n as [| n Hrecn].
  simpl in |- *; apply AbsIR_eq_x; apply less_leEq; apply pos_one.
simpl in |- ×.
eapply eq_transitive_unfolded.
  apply AbsIR_resp_mult.
algebra.
Qed.

Lemma AbsIR_nexp_op : ∀ n x, AbsIR (x [^]n) [=] AbsIR x [^]n.
Proof.
intros; simpl in |- *; apply AbsIR_nexp.
Qed.

Lemma AbsIR_less_square : ∀ x y, AbsIR x [<] y → x [^]2 [<] y [^]2.
Proof.
intros.
eapply less_wdl.
  2: apply AbsIR_eq_x; apply sqr_nonneg.
eapply less_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_nexp_op.
apply nexp_resp_less; auto.
apply AbsIR_nonneg.
Qed.

Lemma AbsIR_leEq_square : ∀ x y, AbsIR x [<=] y → x [^]2 [<=] y [^]2.
Proof.
intros.
eapply leEq_wdl.
  2: apply AbsIR_eq_x; apply sqr_nonneg.
eapply leEq_wdl.
  2: apply eq_symmetric_unfolded; apply AbsIR_nexp_op.
apply nexp_resp_leEq; auto.
apply AbsIR_nonneg.
Qed.

Lemma AbsIR_division : ∀ x y y_ y__, AbsIR (x [/] y [//]y_) [=] (AbsIR x [/] AbsIR y [//]y__).
Proof.
intros x y H Hy.
rstepr (AbsIR x[*] ([1][/] AbsIR y[//]Hy)).
apply eq_transitive_unfolded with (AbsIR (x[*] ([1][/] y[//]H))).
  apply un_op_wd_unfolded; rational.
apply eq_transitive_unfolded with (AbsIR x[*]AbsIR ([1][/] y[//]H)).
  apply AbsIR_resp_mult.
apply mult_wdr.
cut (y [<] [0] or [0] [<] y).
  intros H0.
  elim H0.
   intros.
   apply eq_transitive_unfolded with ( [--] ([1][/] y[//]H)).
    apply AbsIR_eq_inv_x.
    rstepr ([0][/] [--]y[//]inv_resp_ap_zero _ _ H).
    apply shift_leEq_div.
     astepl ( [--]ZeroR).
     apply inv_resp_less; assumption.
    rstepl ( [--]OneR).
    astepr ( [--]ZeroR); apply inv_resp_leEq; apply less_leEq; apply pos_one.
   rstepl ([1][/] [--]y[//]inv_resp_ap_zero _ _ H).
   apply div_wd.
    algebra.
   apply eq_symmetric_unfolded; apply AbsIR_eq_inv_x.
   apply less_leEq; assumption.
  intros.
  apply eq_transitive_unfolded with ([1][/] y[//]H).
   apply AbsIR_eq_x.
   apply less_leEq; apply recip_resp_pos; assumption.
  apply div_wd; [ algebra
    | apply eq_symmetric_unfolded; apply AbsIR_eq_x; apply less_leEq; assumption ].
apply ap_imp_less.
assumption.
Qed.

Some special cases.

Lemma AbsIR_recip : ∀ x x_ x__, AbsIR ([1][/] x [//]x_) [=] ([1][/] AbsIR x [//]x__).
Proof.
intros x H Ha.
apply eq_transitive_unfolded with (AbsIR [1][/] AbsIR x[//]Ha).
  apply AbsIR_division.
apply div_wd.
  2: algebra.
apply AbsIR_eq_x; apply less_leEq; apply pos_one.
Qed.

Lemma AbsIR_div_two : ∀ x, AbsIR (x [/]TwoNZ) [=] AbsIR x [/]TwoNZ.
Proof.
intros.
apply eq_transitive_unfolded with (AbsIR x[/] AbsIR Two [//] AbsIR_resp_ap_zero _
   (ap_symmetric_unfolded _ _ _ (less_imp_ap _ _ _ (pos_two _)))).
  apply AbsIR_division.
apply div_wd.
  algebra.
apply AbsIR_eq_x; apply less_leEq; apply pos_two.
Qed.

Cauchy-Schwartz for IR and variants on that subject.

Lemma triangle_IR : ∀ x y, AbsIR (x [+]y) [<=] AbsIR x [+]AbsIR y.
Proof.
intros.
astepl (sqrt ((x[+]y) [^]2) (sqr_nonneg _ (x[+]y))).
astepr (sqrt (x[^]2) (sqr_nonneg _ x) [+]sqrt (y[^]2) (sqr_nonneg _ y)).
apply power_cancel_leEq with 2. auto.
   astepl ([0][+]ZeroR). apply plus_resp_leEq_both; apply sqrt_nonneg.
  astepl ((x[+]y) [^]2).
rstepl (x[^]2[+]y[^]2[+]Two [*] (x[*]y)).
rstepr (sqrt (x[^]2) (sqr_nonneg IR x) [^]2[+]sqrt (y[^]2) (sqr_nonneg IR y) [^]2[+]
   Two [*] (sqrt (x[^]2) (sqr_nonneg IR x) [*]sqrt (y[^]2) (sqr_nonneg IR y))).
apply plus_resp_leEq_both.
  astepr (x[^]2[+]y[^]2). apply leEq_reflexive.
  apply mult_resp_leEq_lft.
  apply power_cancel_leEq with 2. auto.
    apply mult_resp_nonneg; apply sqrt_nonneg.
  rstepr (sqrt (x[^]2) (sqr_nonneg _ x) [^]2[*]sqrt (y[^]2) (sqr_nonneg _ y) [^]2).
  astepr (x[^]2[*]y[^]2).
  astepl (x[^]2[*]y[^]2).
  apply leEq_reflexive.
apply less_leEq. apply pos_two.
Qed.

Lemma triangle_SumIR : ∀ k l s,
k ≤ S l → AbsIR (Sum k l s) [<=] Sum k l (fun i ⇒ AbsIR (s i)).
Proof.
intros. induction l as [| l Hrecl].
generalize (toCle _ _ H); clear H; intro H.
  inversion H as [|m H0 H1].
   unfold Sum in |- ×. unfold Sum1 in |- ×. simpl in |- ×.
   rstepr ZeroR.
   astepr (AbsIR [0]).
   apply eq_imp_leEq. apply AbsIR_wd. rational.
   inversion H0.
  unfold Sum in |- ×. unfold Sum1 in |- ×. simpl in |- ×.
  rstepr (ABSIR (s 0)).
  apply eq_imp_leEq. apply AbsIR_wd. rational.
  elim (le_lt_eq_dec k (S (S l))); try intro y.
   apply leEq_wdl with (AbsIR (Sum k l s[+]s (S l))).
    apply leEq_wdr with (Sum k l (fun i : nat ⇒ AbsIR (s i)) [+]AbsIR (s (S l))).
     apply leEq_transitive with (AbsIR (Sum k l s) [+]AbsIR (s (S l))).
      apply triangle_IR.
     apply plus_resp_leEq. apply Hrecl. auto with arith.
     apply eq_symmetric_unfolded.
    apply Sum_last with (f := fun i : nat ⇒ AbsIR (s i)).
   apply AbsIR_wd.
   apply eq_symmetric_unfolded. apply Sum_last.
   rewrite y.
  unfold Sum in |- ×. unfold Sum1 in |- ×. simpl in |- ×.
  rstepr ZeroR.
  astepr (AbsIR [0]).
  apply eq_imp_leEq. apply AbsIR_wd. rational.
  auto.
Qed.

Lemma triangle_IR_minus : ∀ x y, AbsIR (x [-]y) [<=] AbsIR x [+]AbsIR y.
Proof.
intros.
unfold cg_minus in |- ×.
apply leEq_wdr with (AbsIR x[+]AbsIR [--]y).
  apply triangle_IR.
apply bin_op_wd_unfolded.
  algebra.
unfold AbsIR in |- *; simpl in |- *; unfold ABSIR in |- ×.
apply eq_transitive_unfolded with (Max [--]y y).
  apply bin_op_wd_unfolded; algebra.
apply Max_comm.
Qed.

Lemma weird_triangleIR : ∀ x y, AbsIR x [-]AbsIR (y [-]x) [<=] AbsIR y.
Proof.
intros.
apply shift_minus_leEq.
simpl in |- *; unfold ABSIR in |- *; apply Max_leEq.
  rstepl (y[+][--] (y[-]x)).
  apply plus_resp_leEq_both; [ apply lft_leEq_Max | apply rht_leEq_Max ].
rstepl ( [--]y[+] (y[-]x)).
apply plus_resp_leEq_both; [ apply rht_leEq_Max | apply lft_leEq_Max ].
Qed.

Lemma triangle_IR_minus' : ∀ x y, AbsIR x [-]AbsIR y [<=] AbsIR (x [-]y).
Proof.
intros.
eapply leEq_wdr.
  2: apply AbsIR_minus.
apply shift_minus_leEq; apply shift_leEq_plus'.
apply weird_triangleIR.
Qed.

Lemma triangle_SumxIR : ∀ n (f : ∀ i, i < n → IR),
AbsIR (Sumx f) [<=] Sumx (fun i H ⇒ AbsIR (f i H)).
Proof.
simple induction n.
  intros; simpl in |- ×.
  apply eq_imp_leEq; apply AbsIRz_isz.
clear n; intros.
simpl in |- *; eapply leEq_transitive.
  apply triangle_IR.
apply plus_resp_leEq.
eapply leEq_wdr.
  apply H.
apply Sumx_wd.
intros; algebra.
Qed.

Lemma triangle_Sum2IR : ∀ m n (f : ∀ i, m ≤ i → i ≤ n → IR),
m ≤ S n → AbsIR (Sum2 f) [<=] Sum2 (fun i Hm Hn ⇒ AbsIR (f i Hm Hn)).
Proof.
intros.
unfold Sum2 in |- ×.
eapply leEq_wdr.
  apply triangle_SumIR.
  assumption.
apply Sum_wd'.
  assumption.
intros.
elim (le_lt_dec m i); intro;
   [ simpl in |- × | elimtype False; apply (le_not_lt m i); auto with arith ].
elim (le_lt_dec i n); intro;
   [ simpl in |- × | elimtype False; apply (le_not_lt i n); auto with arith ].
algebra.
Qed.

Lemma AbsIR_str_bnd_AbsIR : ∀ a b e, AbsIR (a [-]b) [<] e → AbsIR b [<] AbsIR a [+]e.
Proof.
do 3 intro. intro H.
apply shift_less_plus'.
eapply leEq_less_trans.
  apply triangle_IR_minus'.
eapply less_wdl; [ apply H | apply AbsIR_minus ].
Qed.

Lemma AbsIR_bnd_AbsIR : ∀ a b e, AbsIR (a [-]b) [<=] e → AbsIR b [<=] AbsIR a [+]e.
Proof.
intros.
apply shift_leEq_plus'.
eapply leEq_transitive.
  apply triangle_IR_minus'.
eapply leEq_wdl; [ apply H | apply AbsIR_minus ].
Qed.

End Absolute_Props.

Section Consequences.

Cauchy sequences

With these results, we can also prove that the sequence of reciprocals of a Cauchy sequence that is never zero and whose Limit is not zero is also a Cauchy sequence.

Lemma Cauchy_Lim_recip : ∀ seq y, Cauchy_Lim_prop2 seq y →
∀ seq_ y_, Cauchy_Lim_prop2 (fun n : nat ⇒ [1][/] seq n [//]seq_ n) ([1][/] y [//]y_).
Proof.
intros seq y H Hn Hy.
red in |- *; red in H.
intros eps He.
cut {n0 : nat | ∀ n : nat, n0 ≤ n → AbsIR y [/]TwoNZ [<=] AbsIR (seq n)}.
  intro H0.
  elim H0; clear H0; intros n0 Hn0.
  cut ([0] [<] eps [/]TwoNZ [*] (AbsIR y[*]AbsIR y)).
   intro H0.
   elim (H _ H0); clear H.
   intros N HN.
   ∃ (max N n0).
   intros.
   apply AbsIR_imp_AbsSmall.
   apply leEq_wdl with (([1][/] _[//]AbsIR_resp_ap_zero _ (Hn m)) [*]
     ([1][/] _[//]AbsIR_resp_ap_zero _ Hy) [*]AbsIR (seq m[-]y)).
    rstepr ((Two [/] _[//]AbsIR_resp_ap_zero _ Hy) [*] ([1][/] _[//]AbsIR_resp_ap_zero _ Hy) [*]
      (eps [/]TwoNZ [*] (AbsIR y[*]AbsIR y))).
    apply mult_resp_leEq_both.
       astepl (ZeroR [*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive.
        apply less_leEq; apply recip_resp_pos; apply AbsIR_pos; apply Hn.
       apply less_leEq; apply recip_resp_pos; apply AbsIR_pos; apply Hy.
      apply AbsIR_nonneg.
     apply mult_resp_leEq_rht.
      rstepr ([1][/] _[//] div_resp_ap_zero_rev _ _ _ (two_ap_zero _) (AbsIR_resp_ap_zero _ Hy)).
      apply recip_resp_leEq.
       apply pos_div_two; apply AbsIR_pos; apply Hy.
      apply Hn0.
      apply le_trans with (max N n0); auto with arith.
     apply less_leEq; apply recip_resp_pos; apply AbsIR_pos; apply Hy.
    apply AbsSmall_imp_AbsIR.
    apply HN.
    apply le_trans with (max N n0); auto with arith.
   apply eq_transitive_unfolded with
     (AbsIR ([1][/] _[//]Hn m) [*]AbsIR ([1][/] _[//]Hy) [*]AbsIR (y[-]seq m)).
    repeat apply mult_wd; apply eq_symmetric_unfolded.
      apply AbsIR_recip.
     apply AbsIR_recip.
    apply AbsIR_minus.
   apply eq_transitive_unfolded with (AbsIR (([1][/] _[//]Hn m) [*] ([1][/] _[//]Hy) [*] (y[-]seq m))).
    eapply eq_transitive_unfolded.
     2: apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
    apply mult_wdl.
    apply eq_symmetric_unfolded; apply AbsIR_resp_mult.
   apply AbsIR_wd.
   rational.
  astepl (ZeroR [*][0]); apply mult_resp_less_both; try apply leEq_reflexive.
   apply pos_div_two; assumption.
  astepl (ZeroR [*][0]); apply mult_resp_less_both; try apply leEq_reflexive;
    apply AbsIR_pos; apply Hy.
cut {n0 : nat | ∀ n : nat, n0 ≤ n → AbsSmall (AbsIR y [/]TwoNZ) (seq n [-]y)}.
  2: apply H.
  2: eapply less_wdr.
   3: apply AbsIR_div_two.
  2: apply AbsIR_pos.
  2: apply div_resp_ap_zero_rev; apply Hy.
intro H0.
elim H0; intros n0 Hn0; clear H0; ∃ n0; intros.
apply leEq_transitive with (AbsIR y[-]AbsIR (seq n[-]y)).
  apply shift_leEq_minus; apply shift_plus_leEq'.
  rstepr (AbsIR y [/]TwoNZ).
  apply AbsSmall_imp_AbsIR.
  apply Hn0; assumption.
apply weird_triangleIR.
Qed.

Lemma Cauchy_recip : ∀ seq seq_, Lim seq [#] ([0]:IR ) →
Cauchy_prop (fun n ⇒ [1][/] seq n [//]seq_ n).
Proof.
intros seq Hn Hy.
apply Cauchy_prop2_prop.
∃ ([1][/] _[//]Hy).
apply Cauchy_Lim_recip.
apply Cauchy_complete.
Qed.

Lemma Lim_recip : ∀ seq seq_ seq__,
Lim (Build_CauchySeq _ _ (Cauchy_recip seq seq_ seq__)) [=] ([1][/] _[//]seq__).
Proof.
intros.
apply eq_symmetric_unfolded; apply Limits_unique.
simpl in |- *; apply Cauchy_Lim_recip.
apply Cauchy_complete.
Qed.

End Consequences.

Section Part_Function_NRoot.

Functional Operators

Let F:PartIR and denote by P its domain, which must be entirely nonnegative.

Variables F : PartIR.

Let P := Dom F.

Let R := extend P (fun x Hx ⇒ [0][<=]F x Hx).

Let Ext2R := ext2 (P:=P) (R:=fun x Hx ⇒ [0][<=]F x Hx).

Variable n : nat.

Hypothesis Hn : 0 < n.

Lemma part_function_NRoot_strext : ∀ x y Hx Hy,
NRoot (Ext2R x Hx) Hn [#] NRoot (Ext2R y Hy) Hn → x [#] y.
Proof.
intros x y Hx Hy H.
refine (pfstrx _ _ _ _ _ _ (NRoot_str_ext _ _ _ _ _ _ _ H)).
Qed.

Lemma part_function_NRoot_pred_wd : pred_wd _ R.
Proof.
intros x y H H0.
elim H.
intros H1 H2.
split.
apply (dom_wd _ F x y H1 H0).
intros H3.
astepr (F x H1).
auto.
Qed.

Definition FNRoot := Build_PartFunct IR _ part_function_NRoot_pred_wd
(fun x Hx ⇒ NRoot (Ext2R x Hx) Hn) part_function_NRoot_strext.

Section Included.

Variable S:IR → CProp.

Lemma included_FNRoot : included S P →
(∀ x, S x → ∀ Hx, [0][<=]F x Hx) → included S (Dom FNRoot).
Proof.
intros H H0.
simpl in |- ×.
unfold extend in |- ×.
split.
apply H; assumption.
intros; apply H0; assumption.
Qed.

Lemma included_FNRoot' : included S (Dom FNRoot) → included S P.
Proof.
intro H; simpl in H; eapply included_extend; unfold R in *; apply H.
Qed.

End Included.

End Part_Function_NRoot.

Hint Resolve included_FNRoot included_FNRoot' : included.