From f56b37a990555c085f324fbe12da56b2e3a0096c Mon Sep 17 00:00:00 2001
From: desmettr
Date: Tue, 25 Jun 2002 13:27:35 +0000
Subject: Integration de Rcomplet et Alembert_compl

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2806 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Alembert_compl.v | 320 +++++++++++++++++
 theories/Reals/Rcomplet.v       | 737 ++++++++++++++++++++++++++++++++++++++++
 2 files changed, 1057 insertions(+)
 create mode 100644 theories/Reals/Alembert_compl.v
 create mode 100644 theories/Reals/Rcomplet.v

diff --git a/theories/Reals/Alembert_compl.v b/theories/Reals/Alembert_compl.v
new file mode 100644
index 0000000000..a0daa7dd7b
--- /dev/null
+++ b/theories/Reals/Alembert_compl.v
@@ -0,0 +1,320 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(*i $Id$ i*)
+
+Require Max.
+Require Raxioms.
+Require DiscrR.
+Require Rbase.
+Require Rseries.
+Require Rcomplet.
+Require Alembert.
+
+(* Le critère de Cauchy pour les séries *)
+Definition Cauchy_crit_series [An:nat->R] : Prop := (Cauchy_crit [N:nat](sum_f_R0 An N)).
+
+(**********)
+Lemma sum_growing : (An,Bn:nat->R;N:nat) ((n:nat)``(An n)<=(Bn n)``)->``(sum_f_R0 An N)<=(sum_f_R0 Bn N)``.
+Intros.
+Induction N.
+Simpl; Apply H.
+Do 2 Rewrite tech5.
+Apply Rle_trans with ``(sum_f_R0 An N)+(Bn (S N))``.
+Apply Rle_compatibility; Apply H.
+Do 2 Rewrite <- (Rplus_sym (Bn (S N))).
+Apply Rle_compatibility; Apply HrecN.
+Qed.
+
+(**********)
+Lemma Rabsolu_triang_gen : (An:nat->R;N:nat) (Rle (Rabsolu (sum_f_R0 An N)) (sum_f_R0 [i:nat](Rabsolu (An i)) N)). 
+Intros.
+Induction N.
+Simpl.
+Right; Reflexivity.
+Do 2 Rewrite tech5.
+Apply Rle_trans with ``(Rabsolu ((sum_f_R0 An N)))+(Rabsolu (An (S N)))``.
+Apply Rabsolu_triang.
+Do 2 Rewrite <- (Rplus_sym (Rabsolu (An (S N)))).
+Apply Rle_compatibility; Apply HrecN.
+Qed.
+
+(**********)
+Lemma cond_pos_sum : (An:nat->R;N:nat) ((n:nat)``0<=(An n)``) -> ``0<=(sum_f_R0 An N)``.
+Intros.
+Induction N.
+Simpl; Apply H.
+Rewrite tech5.
+Apply ge0_plus_ge0_is_ge0.
+Apply HrecN.
+Apply H.
+Qed.
+
+(* Si (|An|) verifie le critere de Cauchy pour les séries , alors (An) aussi *)
+Lemma cauchy_abs : (An:nat->R) (Cauchy_crit_series [i:nat](Rabsolu (An i))) -> (Cauchy_crit_series An).
+Unfold Cauchy_crit_series; Unfold Cauchy_crit.
+Intros.
+Elim (H eps H0); Intros.
+Exists x.
+Intros.
+Cut (Rle (R_dist (sum_f_R0 An n) (sum_f_R0 An m)) (R_dist (sum_f_R0 [i:nat](Rabsolu (An i)) n) (sum_f_R0 [i:nat](Rabsolu (An i)) m))).
+Intro.
+Apply Rle_lt_trans with (R_dist (sum_f_R0 [i:nat](Rabsolu (An i)) n) (sum_f_R0 [i:nat](Rabsolu (An i)) m)).
+Assumption.
+Apply H1; Assumption.
+Assert H4 := (lt_eq_lt_dec n m).
+Elim H4; Intro.
+Elim a; Intro.
+Rewrite (tech2 An n m); [Idtac | Assumption].
+Rewrite (tech2 [i:nat](Rabsolu (An i)) n m); [Idtac | Assumption].
+Unfold R_dist.
+Unfold Rminus.
+Do 2 Rewrite Ropp_distr1.
+Do 2 Rewrite <- Rplus_assoc.
+Do 2 Rewrite Rplus_Ropp_r.
+Do 2 Rewrite Rplus_Ol.
+Do 2 Rewrite Rabsolu_Ropp.
+Rewrite (Rabsolu_right (sum_f_R0 [i:nat](Rabsolu (An (plus (S n) i))) (minus m (S n)))).
+Pose Bn:=[i:nat](An (plus (S n) i)).
+Replace [i:nat](Rabsolu (An (plus (S n) i))) with [i:nat](Rabsolu (Bn i)).
+Apply Rabsolu_triang_gen.
+Unfold Bn; Reflexivity.
+Apply Rle_sym1.
+Apply cond_pos_sum.
+Intro; Apply Rabsolu_pos.
+Rewrite b.
+Unfold R_dist.
+Unfold Rminus; Do 2 Rewrite Rplus_Ropp_r.
+Rewrite Rabsolu_R0; Right; Reflexivity.
+Rewrite (tech2 An m n); [Idtac | Assumption].
+Rewrite (tech2 [i:nat](Rabsolu (An i)) m n); [Idtac | Assumption].
+Unfold R_dist.
+Unfold Rminus.
+Do 2 Rewrite Rplus_assoc.
+Rewrite (Rplus_sym (sum_f_R0 An m)).
+Rewrite (Rplus_sym (sum_f_R0 [i:nat](Rabsolu (An i)) m)).
+Do 2 Rewrite Rplus_assoc.
+Do 2 Rewrite Rplus_Ropp_l.
+Do 2 Rewrite Rplus_Or.
+Rewrite (Rabsolu_right (sum_f_R0 [i:nat](Rabsolu (An (plus (S m) i))) (minus n (S m)))).
+Pose Bn:=[i:nat](An (plus (S m) i)).
+Replace [i:nat](Rabsolu (An (plus (S m) i))) with [i:nat](Rabsolu (Bn i)).
+Apply Rabsolu_triang_gen.
+Unfold Bn; Reflexivity.
+Apply Rle_sym1.
+Apply cond_pos_sum.
+Intro; Apply Rabsolu_pos.
+Qed.
+
+(**********)
+Lemma cv_cauchy_1 : (An:nat->R) (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)) -> (Cauchy_crit_series An).
+Intros.
+Elim X; Intros.
+Unfold Un_cv in p.
+Unfold Cauchy_crit_series; Unfold Cauchy_crit.
+Intros.
+Cut ``0<eps/2``.
+Intro.
+Elim (p ``eps/2`` H0); Intros.
+Exists x0.
+Intros.
+Apply Rle_lt_trans with ``(R_dist (sum_f_R0 An n) x)+(R_dist (sum_f_R0 An m) x)``.
+Unfold R_dist.
+Replace ``(sum_f_R0 An n)-(sum_f_R0 An m)`` with ``((sum_f_R0 An n)-x)+ -((sum_f_R0 An m)-x)``; [Idtac | Ring].
+Rewrite <- (Rabsolu_Ropp ``(sum_f_R0 An m)-x``).
+Apply Rabsolu_triang.
+Apply Rlt_le_trans with ``eps/2+eps/2``.
+Apply Rplus_lt.
+Apply H1; Assumption.
+Apply H1; Assumption.
+Right; Symmetry; Apply double_var.
+Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
+Qed.
+
+Lemma cv_cauchy_2 : (An:nat->R) (Cauchy_crit_series An) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
+Intros.
+Apply R_complet.
+Unfold Cauchy_crit_series in H.
+Exact H.
+Qed.
+
+Lemma Alembert_strong_general : (An:nat->R;k:R) ``0<=k<1`` -> ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
+Intros.
+Cut (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
+Intro Hyp0; Apply Hyp0.
+Apply cv_cauchy_2.
+Apply cauchy_abs.
+Apply cv_cauchy_1.
+Cut (SigT R [l:R](Un_cv [N:nat](sum_f_R0 [i:nat](Rabsolu (An i)) N) l)) -> (sigTT R [l:R](Un_cv [N:nat](sum_f_R0 [i:nat](Rabsolu (An i)) N) l)).
+Intro Hyp; Apply Hyp.
+Apply (Alembert_strong_positive [i:nat](Rabsolu (An i)) k).
+Assumption.
+Intro; Apply Rabsolu_pos_lt; Apply H0.
+Unfold Un_cv.
+Unfold Un_cv in H1.
+Unfold Rdiv.
+Intros.
+Elim (H1 eps H2); Intros.
+Exists x; Intros.
+Rewrite <- Rabsolu_Rinv.
+Rewrite <- Rabsolu_mult.
+Rewrite Rabsolu_Rabsolu.
+Unfold Rdiv in H3; Apply H3; Assumption.
+Apply H0.
+Intro.
+Elim X; Intros.
+Apply existTT with x.
+Assumption.
+Intro.
+Elim X; Intros.
+Apply Specif.existT with x.
+Assumption.
+Qed.
+
+(* Convergence de la SE dans le disque D(O,1/k) *)
+(* le cas k=0 est decrit par le theoreme "Alembert" *)
+Lemma Alembert_strong : (An:nat->R;x,k:R) ``0<k`` -> ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> ``(Rabsolu x)</k`` -> (SigT R [l:R](Pser An x l)).
+Intros.
+Cut (SigT R [l:R](Un_cv [N:nat](sum_f_R0 [i:nat]``(An i)*(pow x i)`` N) l)).
+Intro.
+Elim X; Intros.
+Apply Specif.existT with x0.
+Apply tech12; Assumption.
+Case (total_order_T x R0); Intro.
+Elim s; Intro.
+EApply Alembert_strong_general with ``k*(Rabsolu x)``.
+Split.
+Unfold Rdiv; Apply Rmult_le_pos.
+Left; Assumption.
+Left; Apply Rabsolu_pos_lt.
+Red; Intro; Rewrite H3 in a; Elim (Rlt_antirefl ? a).
+Apply Rlt_monotony_contra with ``/k``.
+Apply Rlt_Rinv; Assumption.
+Rewrite <- Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l.
+Rewrite Rmult_1r; Assumption.
+Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H).
+Intro; Apply prod_neq_R0.
+Apply H0.
+Apply pow_nonzero.
+Red; Intro; Rewrite H3 in a; Elim (Rlt_antirefl ? a).
+Unfold Un_cv; Unfold Un_cv in H1.
+Intros.
+Cut ``0<eps/(Rabsolu x)``.
+Intro.
+Elim (H1 ``eps/(Rabsolu x)`` H4); Intros.
+Exists x0.
+Intros.
+Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``.
+Unfold R_dist.
+Rewrite Rabsolu_mult.
+Replace ``(Rabsolu ((An (S n))/(An n)))*(Rabsolu x)-k*(Rabsolu x)`` with ``(Rabsolu x)*((Rabsolu ((An (S n))/(An n)))-k)``; [Idtac | Ring].
+Rewrite Rabsolu_mult.
+Rewrite Rabsolu_Rabsolu.
+Apply Rlt_monotony_contra with ``/(Rabsolu x)``.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
+Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a).
+Rewrite <- Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l.
+Rewrite <- (Rmult_sym eps).
+Unfold R_dist in H5.
+Unfold Rdiv; Unfold Rdiv in H5; Apply H5; Assumption.
+Apply Rabsolu_no_R0.
+Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a).
+Unfold Rdiv; Replace (S n) with (plus n (1)); [Idtac | Ring].
+Rewrite pow_add.
+Simpl.
+Rewrite Rmult_1r.
+Rewrite Rinv_Rmult.
+Replace ``(An (plus n (S O)))*((pow x n)*x)*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*/(An n)*x*((pow x n)*/(pow x n))``; [Idtac | Ring].
+Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Reflexivity.
+Apply pow_nonzero.
+Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a).
+Apply H0.
+Apply pow_nonzero.
+Red; Intro; Rewrite H7 in a; Elim (Rlt_antirefl ? a).
+Unfold Rdiv; Apply Rmult_lt_pos.
+Assumption.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
+Red; Intro H7; Rewrite H7 in a; Elim (Rlt_antirefl ? a).
+Apply Specif.existT with (An O).
+Unfold Un_cv.
+Intros.
+Exists O.
+Intros.
+Unfold R_dist.
+Replace (sum_f_R0 [i:nat]``(An i)*(pow x i)`` n) with (An O).
+Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
+Induction n.
+Simpl; Ring.
+Rewrite tech5.
+Rewrite <- Hrecn.
+Rewrite b; Simpl; Ring.
+Unfold ge; Apply le_O_n.
+EApply Alembert_strong_general with ``k*(Rabsolu x)``.
+Split.
+Unfold Rdiv; Apply Rmult_le_pos.
+Left; Assumption.
+Left; Apply Rabsolu_pos_lt.
+Red; Intro; Rewrite H3 in r; Elim (Rlt_antirefl ? r).
+Apply Rlt_monotony_contra with ``/k``.
+Apply Rlt_Rinv; Assumption.
+Rewrite <- Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l.
+Rewrite Rmult_1r; Assumption.
+Red; Intro; Rewrite H3 in H; Elim (Rlt_antirefl ? H).
+Intro; Apply prod_neq_R0.
+Apply H0.
+Apply pow_nonzero.
+Red; Intro; Rewrite H3 in r; Elim (Rlt_antirefl ? r).
+Unfold Un_cv; Unfold Un_cv in H1.
+Intros.
+Cut ``0<eps/(Rabsolu x)``.
+Intro.
+Elim (H1 ``eps/(Rabsolu x)`` H4); Intros.
+Exists x0.
+Intros.
+Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``.
+Unfold R_dist.
+Rewrite Rabsolu_mult.
+Replace ``(Rabsolu ((An (S n))/(An n)))*(Rabsolu x)-k*(Rabsolu x)`` with ``(Rabsolu x)*((Rabsolu ((An (S n))/(An n)))-k)``; [Idtac | Ring].
+Rewrite Rabsolu_mult.
+Rewrite Rabsolu_Rabsolu.
+Apply Rlt_monotony_contra with ``/(Rabsolu x)``.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
+Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r).
+Rewrite <- Rmult_assoc.
+Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l.
+Rewrite <- (Rmult_sym eps).
+Unfold R_dist in H5.
+Unfold Rdiv; Unfold Rdiv in H5; Apply H5; Assumption.
+Apply Rabsolu_no_R0.
+Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r).
+Unfold Rdiv; Replace (S n) with (plus n (1)); [Idtac | Ring].
+Rewrite pow_add.
+Simpl.
+Rewrite Rmult_1r.
+Rewrite Rinv_Rmult.
+Replace ``(An (plus n (S O)))*((pow x n)*x)*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*/(An n)*x*((pow x n)*/(pow x n))``; [Idtac | Ring].
+Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Reflexivity.
+Apply pow_nonzero.
+Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r).
+Apply H0.
+Apply pow_nonzero.
+Red; Intro; Rewrite H7 in r; Elim (Rlt_antirefl ? r).
+Unfold Rdiv; Apply Rmult_lt_pos.
+Assumption.
+Apply Rlt_Rinv; Apply Rabsolu_pos_lt.
+Red; Intro H7; Rewrite H7 in r; Elim (Rlt_antirefl ? r).
+Qed.
\ No newline at end of file
diff --git a/theories/Reals/Rcomplet.v b/theories/Reals/Rcomplet.v
new file mode 100644
index 0000000000..ff601958e4
--- /dev/null
+++ b/theories/Reals/Rcomplet.v
@@ -0,0 +1,737 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+ 
+(*i $Id$ i*)
+
+Require Max.
+Require Raxioms.
+Require DiscrR.
+Require Rbase.
+Require Rseries.
+Require Classical.
+
+
+Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)).
+Definition opp_sui [Un:nat->R] : nat->R := [n:nat]``-(Un n)``.
+Definition majoree [Un:nat->R] : Prop := (bound (EUn Un)).
+Definition minoree [Un:nat->R] : Prop := (bound (EUn (opp_sui Un))).
+
+(* Toute suite croissante et majoree converge *)
+(* Preuve inspiree de celle presente dans Rseries *)
+Lemma growing_cv : (Un:nat->R) (Un_growing Un) -> (majoree Un) -> (sigTT R [l:R](Un_cv Un l)).
+Unfold Un_growing Un_cv;Intros; 
+ Generalize (complet (EUn Un) H0 (EUn_noempty Un));Intro H1.
+ Elim H1;Clear H1;Intros;Split with x;Intros.
+ Unfold is_lub in p;Unfold bound in H0;Unfold is_upper_bound in H0 p.
+ Elim H0;Clear H0;Intros;Elim p;Clear p;Intros;
+ Generalize (H3 x0 H0);Intro;Cut (n:nat)(Rle (Un n) x);Intro.
+Cut (Ex [N:nat] (Rlt (Rminus x eps) (Un N))).
+Intro;Elim H6;Clear H6;Intros;Split with x1.
+Intros;Unfold R_dist;Apply (Rabsolu_def1 (Rminus (Un n) x) eps).
+Unfold Rgt in H1.
+ Apply (Rle_lt_trans (Rminus (Un n) x) R0 eps
+                     (Rle_minus (Un n) x (H5 n)) H1).
+Fold Un_growing in H;Generalize (growing_prop Un n x1 H H7);Intro.
+ Generalize (Rlt_le_trans (Rminus x eps) (Un x1) (Un n) H6
+                          (Rle_sym2 (Un x1) (Un n) H8));Intro;
+ Generalize (Rlt_compatibility (Ropp x) (Rminus x eps) (Un n) H9);
+ Unfold Rminus;Rewrite <-(Rplus_assoc (Ropp x) x (Ropp eps));
+ Rewrite (Rplus_sym (Ropp x) (Un n));Fold (Rminus (Un n) x);
+ Rewrite Rplus_Ropp_l;Rewrite (let (H1,H2)=(Rplus_ne (Ropp eps)) in H2);
+ Trivial.
+Cut ~((N:nat)(Rge (Rminus x eps) (Un N))).
+Intro;Apply (not_all_not_ex nat ([N:nat](Rlt (Rminus x eps) (Un N)))).
+ Red;Intro;Red in H6;Elim H6;Clear H6;Intro;
+ Apply (Rlt_not_ge (Rminus x eps) (Un N) (H7 N)).
+Red;Intro;Cut (N:nat)(Rle (Un N) (Rminus x eps)).
+Intro;Generalize (Un_bound_imp Un (Rminus x eps) H7);Intro;
+ Unfold is_upper_bound in H8;Generalize (H3 (Rminus x eps) H8);Intro;
+ Generalize (Rle_minus x (Rminus x eps) H9);Unfold Rminus;
+ Rewrite Ropp_distr1;Rewrite <- Rplus_assoc;Rewrite Rplus_Ropp_r.
+ Rewrite (let (H1,H2)=(Rplus_ne (Ropp (Ropp eps))) in H2);
+ Rewrite Ropp_Ropp;Intro;Unfold Rgt in H1;
+ Generalize (Rle_not eps R0 H1);Intro;Auto.
+Intro;Elim (H6 N);Intro;Unfold Rle.
+Left;Unfold Rgt in H7;Assumption.
+Right;Auto.
+Apply (H2 (Un n) (Un_in_EUn Un n)).
+Qed.
+
+(* Pour toute suite decroissante, la suite "opposee" est croissante *)
+Lemma decreasing_growing : (Un:nat->R) (Un_decreasing Un) -> (Un_growing (opp_sui Un)).
+Intro.
+Unfold Un_growing opp_sui Un_decreasing.
+Intros.
+Apply Rle_Ropp1.
+Apply H.
+Qed.
+
+(* Toute suite decroissante et minoree converge *)
+Lemma decreasing_cv : (Un:nat->R) (Un_decreasing Un) -> (minoree Un) -> (sigTT R [l:R](Un_cv Un l)).
+Intros.
+Cut (sigTT R [l:R](Un_cv (opp_sui Un) l)) -> (sigTT R [l:R](Un_cv Un l)).
+Intro.
+Apply X.
+Apply growing_cv.
+Apply decreasing_growing; Assumption.
+Exact H0.
+Intro.
+Elim X; Intros.
+Apply existTT with ``-x``.
+Unfold Un_cv in p.
+Unfold R_dist in p.
+Unfold opp_sui in p.
+Unfold Un_cv.
+Unfold R_dist.
+Intros.
+Elim (p eps H1); Intros.
+Exists x0; Intros.
+Assert H4 := (H2 n H3).
+Rewrite <- Rabsolu_Ropp.
+Replace ``-((Un n)- -x)`` with ``-(Un n)-x``; [Assumption | Ring].
+Qed.
+
+(***********)
+Lemma maj_sup : (Un:nat->R) (majoree Un) -> (sigTT R [l:R](is_lub (EUn Un) l)).
+Intros.
+Unfold majoree in H.
+Apply complet.
+Assumption.
+Exists (Un O).
+Unfold EUn.
+Exists O; Reflexivity.
+Qed.
+
+(**********)
+Lemma min_inf : (Un:nat->R) (minoree Un) -> (sigTT R [l:R](is_lub (EUn (opp_sui Un)) l)).
+Intros; Unfold minoree in H.
+Apply complet.
+Assumption.
+Exists ``-(Un O)``.
+Exists O.
+Reflexivity.
+Qed.
+
+Definition majorant [Un:nat->R;pr:(majoree Un)] : R := Cases (maj_sup Un pr) of (existTT a b) => a end.
+
+Definition minorant [Un:nat->R;pr:(minoree Un)] : R := Cases (min_inf Un pr) of (existTT a b) => ``-a`` end.
+
+(* Conservation de la propriete de majoration par extraction *)
+Lemma maj_ss : (Un:nat->R;k:nat) (majoree Un) -> (majoree [i:nat](Un (plus k i))).
+Intros.
+Unfold majoree in H.
+Unfold bound in H.
+Elim H; Intros.
+Unfold is_upper_bound in H0.
+Unfold majoree.
+Exists x.
+Unfold is_upper_bound.
+Intros.
+Apply H0.
+Elim H1; Intros.
+Exists (plus k x1); Assumption.
+Qed.
+
+(* Conservation de la propriete de minoration par extraction *)
+Lemma min_ss : (Un:nat->R;k:nat) (minoree Un) -> (minoree [i:nat](Un (plus k i))).
+Intros.
+Unfold minoree in H.
+Unfold bound in H.
+Elim H; Intros.
+Unfold is_upper_bound in H0.
+Unfold minoree.
+Exists x.
+Unfold is_upper_bound.
+Intros.
+Apply H0.
+Elim H1; Intros.
+Exists (plus k x1); Assumption.
+Qed.
+
+Definition suite_majorant [Un:nat->R;pr:(majoree Un)] : nat -> R := [i:nat](majorant [k:nat](Un (plus i k)) (maj_ss Un i pr)).
+
+Definition suite_minorant [Un:nat->R;pr:(minoree Un)] : nat -> R := [i:nat](minorant [k:nat](Un (plus i k)) (min_ss Un i pr)).
+
+(**********)
+Lemma Rle_Rle_eq : (a,b:R) ``a<=b`` -> ``b<=a`` -> ``a==b``.
+Intros.
+Case (total_order_T a b); Intro.
+Elim s; Intros.
+Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? a0 H0)).
+Assumption.
+Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? r H)).
+Qed.
+
+(* La suite des majorants est decroissante *)
+Lemma Wn_decreasing : (Un:nat->R;pr:(majoree Un)) (Un_decreasing (suite_majorant Un pr)). 
+Intros.
+Unfold Un_decreasing.
+Intro.
+Unfold suite_majorant.
+Assert H := (maj_sup [k:nat](Un (plus (S n) k)) (maj_ss Un (S n) pr)).
+Assert H0 := (maj_sup [k:nat](Un (plus n k)) (maj_ss Un n pr)).
+Elim H; Intros.
+Elim H0; Intros.
+Cut (majorant ([k:nat](Un (plus (S n) k))) (maj_ss Un (S n) pr)) == x; [Intro Maj1; Rewrite Maj1 | Idtac].
+Cut (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr)) == x0; [Intro Maj2; Rewrite Maj2 | Idtac].
+Unfold is_lub in p.
+Unfold is_lub in p0.
+Elim p; Intros.
+Apply H2.
+Elim p0; Intros.
+Unfold is_upper_bound.
+Intros.
+Unfold is_upper_bound in H3.
+Apply H3.
+Elim H5; Intros.
+Exists (plus (1) x2).
+Replace (plus n (plus (S O) x2)) with (plus (S n) x2).
+Assumption.
+Replace (S n) with (plus (1) n); [Ring | Ring].
+Cut (is_lub (EUn [k:nat](Un (plus n k))) (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr))).
+Intro.
+Unfold is_lub in p0; Unfold is_lub in H1.
+Elim p0; Intros; Elim H1; Intros.
+Assert H6 := (H5 x0 H2).
+Assert H7 := (H3 (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr)) H4).
+Apply Rle_Rle_eq; Assumption.
+Unfold majorant.
+Case (maj_sup [k:nat](Un (plus n k)) (maj_ss Un n pr)).
+Trivial.
+Cut (is_lub (EUn [k:nat](Un (plus (S n) k))) (majorant ([k:nat](Un (plus (S n) k))) (maj_ss Un (S n) pr))).
+Intro.
+Unfold is_lub in p; Unfold is_lub in H1.
+Elim p; Intros; Elim H1; Intros.
+Assert H6 := (H5 x H2).
+Assert H7 := (H3 (majorant ([k:nat](Un (plus (S n) k))) (maj_ss Un (S n) pr)) H4).
+Apply Rle_Rle_eq; Assumption.
+Unfold majorant.
+Case (maj_sup [k:nat](Un (plus (S n) k)) (maj_ss Un (S n) pr)).
+Trivial.
+Qed.
+
+(* La suite des minorants est croissante *)
+Lemma Vn_growing : (Un:nat->R;pr:(minoree Un)) (Un_growing (suite_minorant Un pr)).
+Intros.
+Unfold Un_growing.
+Intro.
+Unfold suite_minorant.
+Assert H := (min_inf [k:nat](Un (plus (S n) k)) (min_ss Un (S n) pr)).
+Assert H0 := (min_inf [k:nat](Un (plus n k)) (min_ss Un n pr)).
+Elim H; Intros.
+Elim H0; Intros.
+Cut (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr)) == ``-x``; [Intro Maj1; Rewrite Maj1 | Idtac].
+Cut (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr)) == ``-x0``; [Intro Maj2; Rewrite Maj2 | Idtac].
+Unfold is_lub in p.
+Unfold is_lub in p0.
+Elim p; Intros.
+Apply Rle_Ropp1.
+Apply H2.
+Elim p0; Intros.
+Unfold is_upper_bound.
+Intros.
+Unfold is_upper_bound in H3.
+Apply H3.
+Elim H5; Intros.
+Exists (plus (1) x2).
+Unfold opp_sui in H6.
+Unfold opp_sui.
+Replace (plus n (plus (S O) x2)) with (plus (S n) x2).
+Assumption.
+Replace (S n) with (plus (1) n); [Ring | Ring].
+Cut (is_lub (EUn (opp_sui [k:nat](Un (plus n k)))) (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr)))).
+Intro.
+Unfold is_lub in p0; Unfold is_lub in H1.
+Elim p0; Intros; Elim H1; Intros.
+Assert H6 := (H5 x0 H2).
+Assert H7 := (H3 (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr))) H4).
+Rewrite <- (Ropp_Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr))).
+Apply eq_Ropp; Apply Rle_Rle_eq; Assumption.
+Unfold minorant.
+Case (min_inf [k:nat](Un (plus n k)) (min_ss Un n pr)).
+Intro; Rewrite Ropp_Ropp.
+Trivial.
+Cut (is_lub (EUn (opp_sui [k:nat](Un (plus (S n) k)))) (Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr)))).
+Intro.
+Unfold is_lub in p; Unfold is_lub in H1.
+Elim p; Intros; Elim H1; Intros.
+Assert H6 := (H5 x H2).
+Assert H7 := (H3 (Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr))) H4).
+Rewrite <- (Ropp_Ropp (minorant ([k:nat](Un (plus (S n) k))) (min_ss Un (S n) pr))).
+Apply eq_Ropp; Apply Rle_Rle_eq; Assumption.
+Unfold minorant.
+Case (min_inf [k:nat](Un (plus (S n) k)) (min_ss Un (S n) pr)).
+Intro; Rewrite Ropp_Ropp.
+Trivial.
+Qed.
+
+(* Encadrement Vn,Un,Wn *)
+Lemma Vn_Un_Wn_order : (Un:nat->R;pr1:(majoree Un);pr2:(minoree Un)) (n:nat) ``((suite_minorant Un pr2) n)<=(Un n)<=((suite_majorant Un pr1) n)``. 
+Intros.
+Split.
+Unfold suite_minorant.
+Cut (sigTT R [l:R](is_lub (EUn (opp_sui [i:nat](Un (plus n i)))) l)).
+Intro.
+Elim X; Intros.
+Replace (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2)) with ``-x``.
+Unfold is_lub in p.
+Elim p; Intros.
+Unfold is_upper_bound in H.
+Rewrite <- (Ropp_Ropp (Un n)).
+Apply Rle_Ropp1.
+Apply H.
+Exists O.
+Unfold opp_sui.
+Replace (plus n O) with n; [Reflexivity | Ring].
+Cut (is_lub (EUn (opp_sui [k:nat](Un (plus n k)))) (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2)))).
+Intro.
+Unfold is_lub in p; Unfold is_lub in H.
+Elim p; Intros; Elim H; Intros.
+Assert H4 := (H3 x H0).
+Assert H5 := (H1 (Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2))) H2).
+Rewrite <- (Ropp_Ropp (minorant ([k:nat](Un (plus n k))) (min_ss Un n pr2))).
+Apply eq_Ropp; Apply Rle_Rle_eq; Assumption.
+Unfold minorant.
+Case (min_inf [k:nat](Un (plus n k)) (min_ss Un n pr2)).
+Intro; Rewrite Ropp_Ropp.
+Trivial.
+Apply min_inf.
+Apply min_ss; Assumption.
+Unfold suite_majorant.
+Cut (sigTT R [l:R](is_lub (EUn [i:nat](Un (plus n i))) l)).
+Intro.
+Elim X; Intros.
+Replace (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr1)) with ``x``.
+Unfold is_lub in p.
+Elim p; Intros.
+Unfold is_upper_bound in H.
+Apply H.
+Exists O.
+Replace (plus n O) with n; [Reflexivity | Ring].
+Cut (is_lub (EUn [k:nat](Un (plus n k))) (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr1))).
+Intro.
+Unfold is_lub in p; Unfold is_lub in H.
+Elim p; Intros; Elim H; Intros.
+Assert H4 := (H3 x H0).
+Assert H5 := (H1 (majorant ([k:nat](Un (plus n k))) (maj_ss Un n pr1)) H2).
+Apply Rle_Rle_eq; Assumption.
+Unfold majorant.
+Case (maj_sup [k:nat](Un (plus n k)) (maj_ss Un n pr1)).
+Intro; Trivial.
+Apply maj_sup.
+Apply maj_ss; Assumption.
+Qed.
+
+(* La suite des minorants est majoree *)
+Lemma min_maj : (Un:nat->R;pr1:(majoree Un);pr2:(minoree Un)) (majoree (suite_minorant Un pr2)).
+Intros.
+Assert H := (Vn_Un_Wn_order Un pr1 pr2).
+Unfold majoree.
+Unfold bound.
+Unfold majoree in pr1.
+Unfold bound in pr1.
+Elim pr1; Intros.
+Exists x.
+Unfold is_upper_bound.
+Intros.
+Unfold is_upper_bound in H0.
+Elim H1; Intros.
+Rewrite H2.
+Apply Rle_trans with (Un x1).
+Assert H3 := (H x1); Elim H3; Intros; Assumption.
+Apply H0.
+Exists x1; Reflexivity.
+Qed.
+
+(* La suite des majorants est minoree *)
+Lemma maj_min : (Un:nat->R;pr1:(majoree Un);pr2:(minoree Un)) (minoree (suite_majorant Un pr1)). 
+Intros.
+Assert H := (Vn_Un_Wn_order Un pr1 pr2).
+Unfold minoree.
+Unfold bound.
+Unfold minoree in pr2.
+Unfold bound in pr2.
+Elim pr2; Intros.
+Exists x.
+Unfold is_upper_bound.
+Intros.
+Unfold is_upper_bound in H0.
+Elim H1; Intros.
+Rewrite H2.
+Apply Rle_trans with ((opp_sui Un) x1).
+Assert H3 := (H x1); Elim H3; Intros.
+Unfold opp_sui; Apply Rle_Ropp1.
+Assumption.
+Apply H0.
+Exists x1; Reflexivity.
+Qed.
+
+(* Toute suite de Cauchy est majoree *)
+Lemma cauchy_maj : (Un:nat->R) (Cauchy_crit Un) -> (majoree Un).
+Intros.
+Unfold majoree.
+Apply cauchy_bound.
+Assumption.
+Qed.
+
+(**********)
+Lemma cauchy_opp : (Un:nat->R) (Cauchy_crit Un) -> (Cauchy_crit (opp_sui Un)).
+Intro.
+Unfold Cauchy_crit.
+Unfold R_dist.
+Intros.
+Elim (H eps H0); Intros.
+Exists x; Intros.
+Unfold opp_sui.
+Rewrite <- Rabsolu_Ropp.
+Replace ``-( -(Un n)- -(Un m))`` with ``(Un n)-(Un m)``; [Apply H1; Assumption | Ring].
+Qed.
+
+(* Toute suite de Cauchy est minoree *)
+Lemma cauchy_min : (Un:nat->R) (Cauchy_crit Un) -> (minoree Un).
+Intros.
+Unfold minoree.
+Assert H0 := (cauchy_opp ? H).
+Apply cauchy_bound.
+Assumption.
+Qed.
+
+(* La suite des majorants converge *)
+Lemma maj_cv : (Un:nat->R;pr:(Cauchy_crit Un)) (sigTT R [l:R](Un_cv (suite_majorant Un (cauchy_maj Un pr)) l)).
+Intros.
+Apply decreasing_cv.
+Apply Wn_decreasing.
+Apply maj_min.
+Apply cauchy_min.
+Assumption.
+Qed.
+
+(* La suite des minorants converge *)
+Lemma min_cv : (Un:nat->R;pr:(Cauchy_crit Un)) (sigTT R [l:R](Un_cv (suite_minorant Un (cauchy_min Un pr)) l)).
+Intros.
+Apply growing_cv.
+Apply Vn_growing.
+Apply min_maj.
+Apply cauchy_maj.
+Assumption.
+Qed.
+
+(**********)
+Lemma cond_eq : (x,y:R) ((eps:R)``0<eps``->``(Rabsolu (x-y))<eps``) -> x==y.
+Intros.
+Case (total_order_T x y); Intro.
+Elim s; Intro.
+Cut ``0<y-x``.
+Intro.
+Assert H1 := (H ``y-x`` H0).
+Rewrite <- Rabsolu_Ropp in H1.
+Cut ``-(x-y)==y-x``; [Intro; Rewrite H2 in H1 | Ring].
+Rewrite Rabsolu_right in H1.
+Elim (Rlt_antirefl ? H1).
+Left; Assumption.
+Apply Rlt_anti_compatibility with x.
+Rewrite Rplus_Or; Replace ``x+(y-x)`` with y; [Assumption | Ring].
+Assumption.
+Cut ``0<x-y``.
+Intro.
+Assert H1 := (H ``x-y`` H0).
+Rewrite Rabsolu_right in H1.
+Elim (Rlt_antirefl ? H1).
+Left; Assumption.
+Apply Rlt_anti_compatibility with y.
+Rewrite Rplus_Or; Replace ``y+(x-y)`` with x; [Assumption | Ring].
+Qed.
+
+(**********)
+Lemma not_Rlt : (r1,r2:R)~(``r1<r2``)->``r1>=r2``.
+Intros r1 r2 ; Generalize (total_order r1 r2) ; Unfold Rge.
+Tauto.
+Qed. 
+
+(* On peut approcher la borne sup de toute suite majoree *)
+Lemma approx_maj : (Un:nat->R;pr:(majoree Un)) (eps:R) ``0<eps`` -> (EX k : nat | ``(Rabsolu ((majorant Un pr)-(Un k))) < eps``).
+Intros.
+Pose P := [k:nat]``(Rabsolu ((majorant Un pr)-(Un k))) < eps``.
+Unfold P.
+Cut (EX k:nat | (P k)) -> (EX k:nat | ``(Rabsolu ((majorant Un pr)-(Un k))) < eps``).
+Intros.
+Apply H0.
+Apply not_all_not_ex.
+Red; Intro.
+2:Unfold P; Trivial.
+Unfold P in H1.
+Cut (n:nat)``(Rabsolu ((majorant Un pr)-(Un n))) >= eps``.
+Intro.
+Cut (is_lub (EUn Un) (majorant Un pr)).
+Intro.
+Unfold is_lub in H3.
+Unfold is_upper_bound in H3.
+Elim H3; Intros.
+Cut (n:nat)``eps<=(majorant Un pr)-(Un n)``.
+Intro.
+Cut (n:nat)``(Un n)<=(majorant Un pr)-eps``.
+Intro.
+Cut ((x:R)(EUn Un x)->``x <= (majorant Un pr)-eps``).
+Intro.
+Assert H9 := (H5 ``(majorant Un pr)-eps`` H8).
+Cut ``eps<=0``.
+Intro.
+Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H H10)).
+Apply Rle_anti_compatibility with ``(majorant Un pr)-eps``.
+Rewrite Rplus_Or.
+Replace ``(majorant Un pr)-eps+eps`` with (majorant Un pr); [Assumption | Ring].
+Intros.
+Unfold EUn in H8.
+Elim H8; Intros.
+Rewrite H9; Apply H7.
+Intro.
+Assert H7 := (H6 n).
+Apply Rle_anti_compatibility with ``eps-(Un n)``.
+Replace ``eps-(Un n)+(Un n)`` with ``eps``.
+Replace ``eps-(Un n)+((majorant Un pr)-eps)`` with ``(majorant Un pr)-(Un n)``.
+Assumption.
+Ring.
+Ring.
+Intro.
+Assert H6 := (H2 n).
+Rewrite Rabsolu_right in H6.
+Apply Rle_sym2.
+Assumption.
+Apply Rle_sym1.
+Apply Rle_anti_compatibility with (Un n).
+Rewrite Rplus_Or; Replace ``(Un n)+((majorant Un pr)-(Un n))`` with (majorant Un pr); [Apply H4 | Ring].
+Exists n; Reflexivity.
+Unfold majorant.
+Case (maj_sup Un pr).
+Trivial.
+Intro.
+Assert H2 := (H1 n).
+Apply not_Rlt; Assumption.
+Qed.
+
+(* On peut approcher la borne inf de toute suite minoree *)
+Lemma approx_min : (Un:nat->R;pr:(minoree Un)) (eps:R) ``0<eps`` -> (EX k :nat | ``(Rabsolu ((minorant Un pr)-(Un k))) < eps``).
+Intros.
+Pose P := [k:nat]``(Rabsolu ((minorant Un pr)-(Un k))) < eps``.
+Unfold P.
+Cut (EX k:nat | (P k)) -> (EX k:nat | ``(Rabsolu ((minorant Un pr)-(Un k))) < eps``).
+Intros.
+Apply H0.
+Apply not_all_not_ex.
+Red; Intro.
+2:Unfold P; Trivial.
+Unfold P in H1.
+Cut (n:nat)``(Rabsolu ((minorant Un pr)-(Un n))) >= eps``.
+Intro.
+Cut (is_lub (EUn (opp_sui Un)) ``-(minorant Un pr)``).
+Intro.
+Unfold is_lub in H3.
+Unfold is_upper_bound in H3.
+Elim H3; Intros.
+Cut (n:nat)``eps<=(Un n)-(minorant Un pr)``.
+Intro.
+Cut (n:nat)``((opp_sui Un) n)<=-(minorant Un pr)-eps``.
+Intro.
+Cut ((x:R)(EUn (opp_sui Un) x)->``x <= -(minorant Un pr)-eps``).
+Intro.
+Assert H9 := (H5 ``-(minorant Un pr)-eps`` H8).
+Cut ``eps<=0``.
+Intro.
+Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H H10)).
+Apply Rle_anti_compatibility with ``-(minorant Un pr)-eps``.
+Rewrite Rplus_Or.
+Replace ``-(minorant Un pr)-eps+eps`` with ``-(minorant Un pr)``; [Assumption | Ring].
+Intros.
+Unfold EUn in H8.
+Elim H8; Intros.
+Rewrite H9; Apply H7.
+Intro.
+Assert H7 := (H6 n).
+Unfold opp_sui.
+Apply Rle_anti_compatibility with ``eps+(Un n)``.
+Replace ``eps+(Un n)+ -(Un n)`` with ``eps``.
+Replace ``eps+(Un n)+(-(minorant Un pr)-eps)`` with ``(Un n)-(minorant Un pr)``.
+Assumption.
+Ring.
+Ring.
+Intro.
+Assert H6 := (H2 n).
+Rewrite Rabsolu_left1 in H6.
+Apply Rle_sym2.
+Replace ``(Un n)-(minorant Un pr)`` with `` -((minorant Un pr)-(Un n))``; [Assumption | Ring].
+Apply Rle_anti_compatibility with ``-(minorant Un pr)``.
+Rewrite Rplus_Or; Replace ``-(minorant Un pr)+((minorant Un pr)-(Un n))`` with ``-(Un n)``.
+Apply H4.
+Exists n; Reflexivity.
+Ring.
+Unfold minorant.
+Case (min_inf Un pr).
+Intro.
+Rewrite Ropp_Ropp.
+Trivial.
+Intro.
+Assert H2 := (H1 n).
+Apply not_Rlt; Assumption.
+Qed.
+
+(****************************************************)
+(*              R est complet :                     *)
+(*    Toute suite de Cauchy de (R,| |) converge     *)
+(*                                                  *)
+(*  Preuve a l'aide des suites adjacentes Vn et Wn  *)
+(****************************************************)
+
+Theorem R_complet : (Un:nat->R) (Cauchy_crit Un) -> (sigTT R [l:R](Un_cv Un l)).
+Intros.
+Pose Vn := (suite_minorant Un (cauchy_min Un H)).
+Pose Wn := (suite_majorant Un (cauchy_maj Un H)).
+Assert H0 := (maj_cv Un H).
+Fold Wn in H0.
+Assert H1 := (min_cv Un H).
+Fold Vn in H1.
+Elim H0; Intros.
+Elim H1; Intros.
+Cut x==x0.
+Intros.
+Apply existTT with x.
+Rewrite <- H2 in p0.
+Unfold Un_cv.
+Intros.
+Unfold Un_cv in p; Unfold Un_cv in p0.
+Cut ``0<eps/3``.
+Intro.
+Elim (p ``eps/3`` H4); Intros.
+Elim (p0 ``eps/3`` H4); Intros.
+Exists (max x1 x2).
+Intros.
+Unfold R_dist.
+Apply Rle_lt_trans with ``(Rabsolu ((Un n)-(Vn n)))+(Rabsolu ((Vn n)-x))``.
+Replace ``(Un n)-x`` with ``((Un n)-(Vn n))+((Vn n)-x)``; [Apply Rabsolu_triang | Ring].
+Apply Rle_lt_trans with ``(Rabsolu ((Wn n)-(Vn n)))+(Rabsolu ((Vn n)-x))``.
+Do 2 Rewrite <- (Rplus_sym ``(Rabsolu ((Vn n)-x))``).
+Apply Rle_compatibility.
+Repeat Rewrite Rabsolu_right.
+Unfold Rminus; Do 2 Rewrite <- (Rplus_sym ``-(Vn n)``); Apply Rle_compatibility.
+Assert H8 := (Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
+Fold Vn Wn in H8.
+Elim (H8 n); Intros.
+Assumption.
+Apply Rle_sym1.
+Unfold Rminus; Apply Rle_anti_compatibility with (Vn n).
+Rewrite Rplus_Or.
+Replace ``(Vn n)+((Wn n)+ -(Vn n))`` with (Wn n); [Idtac | Ring].
+Assert H8 := (Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
+Fold Vn Wn in H8.
+Elim (H8 n); Intros.
+Apply Rle_trans with (Un n); Assumption.
+Apply Rle_sym1.
+Unfold Rminus; Apply Rle_anti_compatibility with (Vn n).
+Rewrite Rplus_Or.
+Replace ``(Vn n)+((Un n)+ -(Vn n))`` with (Un n); [Idtac | Ring].
+Assert H8 := (Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
+Fold Vn Wn in H8.
+Elim (H8 n); Intros.
+Assumption.
+Apply Rle_lt_trans with ``(Rabsolu ((Wn n)-x))+(Rabsolu (x-(Vn n)))+(Rabsolu ((Vn n)-x))``.
+Do 2 Rewrite <- (Rplus_sym ``(Rabsolu ((Vn n)-x))``).
+Apply Rle_compatibility.
+Replace ``(Wn n)-(Vn n)`` with ``((Wn n)-x)+(x-(Vn n))``; [Apply Rabsolu_triang | Ring].
+Apply Rlt_le_trans with ``eps/3+eps/3+eps/3``.
+Repeat Apply Rplus_lt.
+Unfold R_dist in H5.
+Apply H5.
+Unfold ge; Apply le_trans with (max x1 x2).
+Apply le_max_l.
+Assumption.
+Rewrite <- Rabsolu_Ropp.
+Replace ``-(x-(Vn n))`` with ``(Vn n)-x``; [Idtac | Ring].
+Unfold R_dist in H6.
+Apply H6.
+Unfold ge; Apply le_trans with (max x1 x2).
+Apply le_max_r.
+Assumption.
+Unfold R_dist in H6.
+Apply H6.
+Unfold ge; Apply le_trans with (max x1 x2).
+Apply le_max_r.
+Assumption.
+Right.
+Pattern 4 eps; Replace ``eps`` with ``3*eps/3``.
+Ring.
+Unfold Rdiv; Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; DiscrR.
+Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0].
+Apply cond_eq.
+Intros.
+Cut ``0<eps/5``.
+Intro.
+Unfold Un_cv in p; Unfold Un_cv in p0.
+Unfold R_dist in p; Unfold R_dist in p0.
+Elim (p ``eps/5`` H3); Intros N1 H4.
+Elim (p0 ``eps/5`` H3); Intros N2 H5.
+Unfold Cauchy_crit in H.
+Unfold R_dist in H.
+Elim (H ``eps/5`` H3); Intros N3 H6.
+Pose N := (max (max N1 N2) N3).
+Apply Rle_lt_trans with ``(Rabsolu (x-(Wn N)))+(Rabsolu ((Wn N)-x0))``.
+Replace ``x-x0`` with ``(x-(Wn N))+((Wn N)-x0)``; [Apply Rabsolu_triang | Ring].
+Apply Rle_lt_trans with ``(Rabsolu (x-(Wn N)))+(Rabsolu ((Wn N)-(Vn N)))+(Rabsolu (((Vn N)-x0)))``.
+Rewrite Rplus_assoc.
+Apply Rle_compatibility.
+Replace ``(Wn N)-x0`` with ``((Wn N)-(Vn N))+((Vn N)-x0)``; [Apply Rabsolu_triang | Ring].
+Replace ``eps`` with ``eps/5+3*eps/5+eps/5``.
+Repeat Apply Rplus_lt.
+Rewrite <- Rabsolu_Ropp.
+Replace ``-(x-(Wn N))`` with ``(Wn N)-x``; [Apply H4 | Ring].
+Unfold ge N.
+Apply le_trans with (max N1 N2); Apply le_max_l.
+Unfold Wn Vn.
+Unfold suite_majorant suite_minorant.
+Assert H7 := (approx_maj [k:nat](Un (plus N k)) (maj_ss Un N (cauchy_maj Un H))).
+Assert H8 := (approx_min [k:nat](Un (plus N k)) (min_ss Un N (cauchy_min Un H))).
+Cut (Wn N)==(majorant ([k:nat](Un (plus N k))) (maj_ss Un N (cauchy_maj Un H))).
+Cut (Vn N)==(minorant ([k:nat](Un (plus N k))) (min_ss Un N (cauchy_min Un H))).
+Intros.
+Rewrite <- H9; Rewrite <- H10.
+Rewrite <- H9 in H8.
+Rewrite <- H10 in H7.
+Elim (H7 ``eps/5`` H3); Intros k2 H11.
+Elim (H8 ``eps/5`` H3); Intros k1 H12.
+Apply Rle_lt_trans with ``(Rabsolu ((Wn N)-(Un (plus N k2))))+(Rabsolu ((Un (plus N k2))-(Vn N)))``.
+Replace ``(Wn N)-(Vn N)`` with ``((Wn N)-(Un (plus N k2)))+((Un (plus N k2))-(Vn N))``; [Apply Rabsolu_triang | Ring].
+Apply Rle_lt_trans with ``(Rabsolu ((Wn N)-(Un (plus N k2))))+(Rabsolu ((Un (plus N k2))-(Un (plus N k1))))+(Rabsolu ((Un (plus N k1))-(Vn N)))``.
+Rewrite Rplus_assoc.
+Apply Rle_compatibility.
+Replace ``(Un (plus N k2))-(Vn N)`` with ``((Un (plus N k2))-(Un (plus N k1)))+((Un (plus N k1))-(Vn N))``; [Apply Rabsolu_triang | Ring].
+Replace ``3*eps/5`` with ``eps/5+eps/5+eps/5``; [Repeat Apply Rplus_lt | Ring].
+Assumption.
+Apply H6.
+Unfold ge.
+Apply le_trans with N.
+Unfold N; Apply le_max_r.
+Apply le_plus_l.
+Unfold ge.
+Apply le_trans with N.
+Unfold N; Apply le_max_r.
+Apply le_plus_l.
+Rewrite <- Rabsolu_Ropp.
+Replace ``-((Un (plus N k1))-(Vn N))`` with ``(Vn N)-(Un (plus N k1))``; [Assumption | Ring].
+Reflexivity.
+Reflexivity.
+Apply H5.
+Unfold ge; Apply le_trans with (max N1 N2).
+Apply le_max_r.
+Unfold N; Apply le_max_l.
+Pattern 4 eps; Replace ``eps`` with ``5*eps/5``.
+Ring.
+Unfold Rdiv; Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m.
+DiscrR.
+Unfold Rdiv; Apply Rmult_lt_pos.
+Assumption.
+Apply Rlt_Rinv.
+Sup0; Try Apply lt_O_Sn.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3