diff options
author | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
---|---|---|
committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-27 21:18:40 +0000 |
commit | bcc5b59c086d1c06a1ec03ee0bff7647338bb258 (patch) | |
tree | 4f332b460941cdbb211806659b1fe76253f2fc67 /theories/Reals/PSeries_reg.v | |
parent | 35cd1baf98895aa07d300d22c9e8148c91b43dac (diff) |
Réorganisation de la librairie des réels
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3311 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/PSeries_reg.v')
-rw-r--r-- | theories/Reals/PSeries_reg.v | 332 |
1 files changed, 3 insertions, 329 deletions
diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 743e1184d..d056387f4 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -8,18 +8,9 @@ (*i $Id$ i*) -Require Rbase. -Require DiscrR. +Require RealsB. Require Rfunctions. -Require Rseries. -Require Rsigma. -Require Alembert. -Require Alembert_compl. -Require Binome. -Require Cv_prop. -Require Rcomplet. -Require Rtrigo_alt. -Require Cos_plus. +Require SeqSeries. Require Ranalysis1. Require Max. Require Even. @@ -32,286 +23,8 @@ Definition CVN_r [fn:nat->R->R;r:posreal] : Type := (SigT ? [An:nat->R](sigTT R Definition CVN_R [fn:nat->R->R] : Type := (r:posreal) (CVN_r fn r). -Definition SP [fn:nat->R->R;N:nat] : R->R := [x:R](sum_f_R0 [k:nat]``(fn k x)`` N). - Definition SFL [fn:nat->R->R;cv:(x:R)(sigTT ? [l:R](Un_cv [N:nat](SP fn N x) l))] : R-> R := [y:R](Cases (cv y) of (existTT a b) => a end). -(**********) -Lemma sum_incr : (An:nat->R;N:nat;l:R) (Un_cv [n:nat](sum_f_R0 An n) l) -> ((n:nat)``0<=(An n)``) -> ``(sum_f_R0 An N)<=l``. -Intros; Case (total_order_T (sum_f_R0 An N) l); Intro. -Elim s; Intro. -Left; Apply a. -Right; Apply b. -Cut (Un_growing [n:nat](sum_f_R0 An n)). -Intro; Pose l1 := (sum_f_R0 An N). -Fold l1 in r. -Unfold Un_cv in H; Cut ``0<l1-l``. -Intro; Elim (H ? H2); Intros. -Pose N0 := (max x N); Cut (ge N0 x). -Intro; Assert H5 := (H3 N0 H4). -Cut ``l1<=(sum_f_R0 An N0)``. -Intro; Unfold R_dist in H5; Rewrite Rabsolu_right in H5. -Cut ``(sum_f_R0 An N0)<l1``. -Intro; Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H7 H6)). -Apply Rlt_anti_compatibility with ``-l``. -Do 2 Rewrite (Rplus_sym ``-l``). -Apply H5. -Apply Rle_sym1; Apply Rle_anti_compatibility with l. -Rewrite Rplus_Or; Replace ``l+((sum_f_R0 An N0)-l)`` with (sum_f_R0 An N0); [Idtac | Ring]; Apply Rle_trans with l1. -Left; Apply r. -Apply H6. -Unfold l1; Apply Rle_sym2; Apply (growing_prop [k:nat](sum_f_R0 An k)). -Apply H1. -Unfold ge N0; Apply le_max_r. -Unfold ge N0; Apply le_max_l. -Apply Rlt_anti_compatibility with l; Rewrite Rplus_Or; Replace ``l+(l1-l)`` with l1; [Apply r | Ring]. -Unfold Un_growing; Intro; Simpl; Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or; Apply Rle_compatibility; Apply H0. -Qed. - -(**********) -Lemma sum_cv_maj : (An:nat->R;fn:nat->R->R;x,l1,l2:R) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu l1)<=l2``. -Intros; Case (total_order_T (Rabsolu l1) l2); Intro. -Elim s; Intro. -Left; Apply a. -Right; Apply b. -Cut (n0:nat)``(Rabsolu (SP fn n0 x))<=(sum_f_R0 An n0)``. -Intro; Cut ``0<((Rabsolu l1)-l2)/2``. -Intro; Unfold Un_cv in H H0. -Elim (H ? H3); Intros Na H4. -Elim (H0 ? H3); Intros Nb H5. -Pose N := (max Na Nb). -Unfold R_dist in H4 H5. -Cut ``(Rabsolu ((sum_f_R0 An N)-l2))<((Rabsolu l1)-l2)/2``. -Intro; Cut ``(Rabsolu ((Rabsolu l1)-(Rabsolu (SP fn N x))))<((Rabsolu l1)-l2)/2``. -Intro; Cut ``(sum_f_R0 An N)<((Rabsolu l1)+l2)/2``. -Intro; Cut ``((Rabsolu l1)+l2)/2<(Rabsolu (SP fn N x))``. -Intro; Cut ``(sum_f_R0 An N)<(Rabsolu (SP fn N x))``. -Intro; Assert H11 := (H2 N). -Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H11 H10)). -Apply Rlt_trans with ``((Rabsolu l1)+l2)/2``; Assumption. -Case (case_Rabsolu ``(Rabsolu l1)-(Rabsolu (SP fn N x))``); Intro. -Apply Rlt_trans with (Rabsolu l1). -Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -Unfold Rdiv; Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite double; Apply Rlt_compatibility; Apply r. -DiscrR. -Apply (Rminus_lt ? ? r0). -Rewrite (Rabsolu_right ? r0) in H7. -Apply Rlt_anti_compatibility with ``((Rabsolu l1)-l2)/2-(Rabsolu (SP fn N x))``. -Replace ``((Rabsolu l1)-l2)/2-(Rabsolu (SP fn N x))+((Rabsolu l1)+l2)/2`` with ``(Rabsolu l1)-(Rabsolu (SP fn N x))``. -Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply H7. -Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Rewrite <- (Rmult_sym ``/2``); Rewrite Rminus_distr; Repeat Rewrite (Rmult_sym ``/2``); Pattern 1 (Rabsolu l1); Rewrite double_var; Unfold Rdiv; Ring. -Case (case_Rabsolu ``(sum_f_R0 An N)-l2``); Intro. -Apply Rlt_trans with l2. -Apply (Rminus_lt ? ? r0). -Apply Rlt_monotony_contra with ``2``. -Apply Rgt_2_0. -Rewrite (double l2); Unfold Rdiv; Rewrite (Rmult_sym ``2``); Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym. -Rewrite Rmult_1r; Rewrite (Rplus_sym (Rabsolu l1)); Apply Rlt_compatibility; Apply r. -DiscrR. -Rewrite (Rabsolu_right ? r0) in H6; Apply Rlt_anti_compatibility with ``-l2``. -Replace ``-l2+((Rabsolu l1)+l2)/2`` with ``((Rabsolu l1)-l2)/2``. -Rewrite Rplus_sym; Apply H6. -Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Rewrite Rminus_distr; Rewrite Rmult_Rplus_distrl; Pattern 2 l2; Rewrite double_var; Repeat Rewrite (Rmult_sym ``/2``); Rewrite Ropp_distr1; Unfold Rdiv; Ring. -Apply Rle_lt_trans with ``(Rabsolu ((SP fn N x)-l1))``. -Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr3; Apply Rabsolu_triang_inv2. -Apply H4; Unfold ge N; Apply le_max_l. -Apply H5; Unfold ge N; Apply le_max_r. -Unfold Rdiv; Apply Rmult_lt_pos. -Apply Rlt_anti_compatibility with l2. -Rewrite Rplus_Or; Replace ``l2+((Rabsolu l1)-l2)`` with (Rabsolu l1); [Apply r | Ring]. -Apply Rlt_Rinv; Apply Rgt_2_0. -Intros; Induction n0. -Unfold SP; Simpl; Apply H1. -Unfold SP; Simpl. -Apply Rle_trans with (Rplus (Rabsolu (sum_f_R0 [k:nat](fn k x) n0)) (Rabsolu (fn (S n0) x))). -Apply Rabsolu_triang. -Apply Rle_trans with ``(sum_f_R0 An n0)+(Rabsolu (fn (S n0) x))``. -Do 2 Rewrite <- (Rplus_sym (Rabsolu (fn (S n0) x))). -Apply Rle_compatibility; Apply Hrecn0. -Apply Rle_compatibility; Apply H1. -Qed. - -(**********) -Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``. -Intros; Cut (sigTT R [l:R](Un_cv [n:nat](sum_f_R0 [l:nat](fn (plus (S N) l) x) n) l)). -Intro; Cut (sigTT R [l:R](Un_cv [n:nat](sum_f_R0 [l:nat](An (plus (S N) l)) n) l)). -Intro; Elim X; Intros l1N H2. -Elim X0; Intros l2N H3. -Cut ``l1-(SP fn N x)==l1N``. -Intro; Cut ``l2-(sum_f_R0 An N)==l2N``. -Intro; Rewrite H4; Rewrite H5. -Apply sum_cv_maj with [l:nat](An (plus (S N) l)) [l:nat][x:R](fn (plus (S N) l) x) x. -Unfold SP; Apply H2. -Apply H3. -Intros; Apply H1. -Symmetry; EApply UL_suite. -Apply H3. -Unfold Un_cv in H0; Unfold Un_cv; Intros; Elim (H0 eps H5); Intros N0 H6. -Unfold R_dist in H6; Exists N0; Intros. -Unfold R_dist; Replace (Rminus (sum_f_R0 [l:nat](An (plus (S N) l)) n) (Rminus l2 (sum_f_R0 An N))) with (Rminus (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) l2); [Idtac | Ring]. -Replace (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) with (sum_f_R0 An (S (plus N n))). -Apply H6; Unfold ge; Apply le_trans with n. -Apply H7. -Apply le_trans with (plus N n). -Apply le_plus_r. -Apply le_n_Sn. -Cut (le O N). -Cut (lt N (S (plus N n))). -Intros; Assert H10 := (sigma_split An H9 H8). -Unfold sigma in H10. -Do 2 Rewrite <- minus_n_O in H10. -Replace (sum_f_R0 An (S (plus N n))) with (sum_f_R0 [k:nat](An (plus (0) k)) (S (plus N n))). -Replace (sum_f_R0 An N) with (sum_f_R0 [k:nat](An (plus (0) k)) N). -Cut (minus (S (plus N n)) (S N))=n. -Intro; Rewrite H11 in H10. -Apply H10. -Apply INR_eq; Rewrite minus_INR. -Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_n_S; Apply le_plus_l. -Apply sum_eq; Intros. -Reflexivity. -Apply sum_eq; Intros. -Reflexivity. -Apply le_lt_n_Sm; Apply le_plus_l. -Apply le_O_n. -Symmetry; EApply UL_suite. -Apply H2. -Unfold Un_cv in H; Unfold Un_cv; Intros. -Elim (H eps H4); Intros N0 H5. -Unfold R_dist in H5; Exists N0; Intros. -Unfold R_dist SP; Replace (Rminus (sum_f_R0 [l:nat](fn (plus (S N) l) x) n) (Rminus l1 (sum_f_R0 [k:nat](fn k x) N))) with (Rminus (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) l1); [Idtac | Ring]. -Replace (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) with (sum_f_R0 [k:nat](fn k x) (S (plus N n))). -Unfold SP in H5; Apply H5; Unfold ge; Apply le_trans with n. -Apply H6. -Apply le_trans with (plus N n). -Apply le_plus_r. -Apply le_n_Sn. -Cut (le O N). -Cut (lt N (S (plus N n))). -Intros; Assert H9 := (sigma_split [k:nat](fn k x) H8 H7). -Unfold sigma in H9. -Do 2 Rewrite <- minus_n_O in H9. -Replace (sum_f_R0 [k:nat](fn k x) (S (plus N n))) with (sum_f_R0 [k:nat](fn (plus (0) k) x) (S (plus N n))). -Replace (sum_f_R0 [k:nat](fn k x) N) with (sum_f_R0 [k:nat](fn (plus (0) k) x) N). -Cut (minus (S (plus N n)) (S N))=n. -Intro; Rewrite H10 in H9. -Apply H9. -Apply INR_eq; Rewrite minus_INR. -Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_n_S; Apply le_plus_l. -Apply sum_eq; Intros. -Reflexivity. -Apply sum_eq; Intros. -Reflexivity. -Apply le_lt_n_Sm. -Apply le_plus_l. -Apply le_O_n. -Apply existTT with ``l2-(sum_f_R0 An N)``. -Unfold Un_cv in H0; Unfold Un_cv; Intros. -Elim (H0 eps H2); Intros N0 H3. -Unfold R_dist in H3; Exists N0; Intros. -Unfold R_dist; Replace (Rminus (sum_f_R0 [l:nat](An (plus (S N) l)) n) (Rminus l2 (sum_f_R0 An N))) with (Rminus (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) l2); [Idtac | Ring]. -Replace (Rplus (sum_f_R0 An N) (sum_f_R0 [l:nat](An (plus (S N) l)) n)) with (sum_f_R0 An (S (plus N n))). -Apply H3; Unfold ge; Apply le_trans with n. -Apply H4. -Apply le_trans with (plus N n). -Apply le_plus_r. -Apply le_n_Sn. -Cut (le O N). -Cut (lt N (S (plus N n))). -Intros; Assert H7 := (sigma_split An H6 H5). -Unfold sigma in H7. -Do 2 Rewrite <- minus_n_O in H7. -Replace (sum_f_R0 An (S (plus N n))) with (sum_f_R0 [k:nat](An (plus (0) k)) (S (plus N n))). -Replace (sum_f_R0 An N) with (sum_f_R0 [k:nat](An (plus (0) k)) N). -Cut (minus (S (plus N n)) (S N))=n. -Intro; Rewrite H8 in H7. -Apply H7. -Apply INR_eq; Rewrite minus_INR. -Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_n_S; Apply le_plus_l. -Apply sum_eq; Intros. -Reflexivity. -Apply sum_eq; Intros. -Reflexivity. -Apply le_lt_n_Sm. -Apply le_plus_l. -Apply le_O_n. -Apply existTT with ``l1-(SP fn N x)``. -Unfold Un_cv in H; Unfold Un_cv; Intros. -Elim (H eps H2); Intros N0 H3. -Unfold R_dist in H3; Exists N0; Intros. -Unfold R_dist SP. -Replace (Rminus (sum_f_R0 [l:nat](fn (plus (S N) l) x) n) (Rminus l1 (sum_f_R0 [k:nat](fn k x) N))) with (Rminus (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) l1); [Idtac | Ring]. -Replace (Rplus (sum_f_R0 [k:nat](fn k x) N) (sum_f_R0 [l:nat](fn (plus (S N) l) x) n)) with (sum_f_R0 [k:nat](fn k x) (S (plus N n))). -Unfold SP in H3; Apply H3. -Unfold ge; Apply le_trans with n. -Apply H4. -Apply le_trans with (plus N n). -Apply le_plus_r. -Apply le_n_Sn. -Cut (le O N). -Cut (lt N (S (plus N n))). -Intros; Assert H7 := (sigma_split [k:nat](fn k x) H6 H5). -Unfold sigma in H7. -Do 2 Rewrite <- minus_n_O in H7. -Replace (sum_f_R0 [k:nat](fn k x) (S (plus N n))) with (sum_f_R0 [k:nat](fn (plus (0) k) x) (S (plus N n))). -Replace (sum_f_R0 [k:nat](fn k x) N) with (sum_f_R0 [k:nat](fn (plus (0) k) x) N). -Cut (minus (S (plus N n)) (S N))=n. -Intro; Rewrite H8 in H7. -Apply H7. -Apply INR_eq; Rewrite minus_INR. -Do 2 Rewrite S_INR; Rewrite plus_INR; Ring. -Apply le_n_S; Apply le_plus_l. -Apply sum_eq; Intros. -Reflexivity. -Apply sum_eq; Intros. -Reflexivity. -Apply le_lt_n_Sm. -Apply le_plus_l. -Apply le_O_n. -Qed. - -Lemma pow1 : (n:nat) (pow R1 n)==R1. -Intro; Induction n. -Reflexivity. -Simpl; Rewrite Hrecn; Rewrite Rmult_1r; Reflexivity. -Qed. - -Lemma pow_Rabs : (x:R;n:nat) ``(pow x n)<=(pow (Rabsolu x) n)``. -Intros; Induction n. -Right; Reflexivity. -Simpl; Case (case_Rabsolu x); Intro. -Apply Rle_trans with (Rabsolu ``x*(pow x n)``). -Apply Rle_Rabsolu. -Rewrite Rabsolu_mult. -Apply Rle_monotony. -Apply Rabsolu_pos. -Right; Symmetry; Apply Pow_Rabsolu. -Pattern 1 (Rabsolu x); Rewrite (Rabsolu_right x r); Apply Rle_monotony. -Apply Rle_sym2; Exact r. -Apply Hrecn. -Qed. - -Lemma pow_maj_Rabs : (x,y:R;n:nat) ``(Rabsolu y)<=x`` -> ``(pow y n)<=(pow x n)``. -Intros; Cut ``0<=x``. -Intro; Apply Rle_trans with (pow (Rabsolu y) n). -Apply pow_Rabs. -Induction n. -Right; Reflexivity. -Simpl; Apply Rle_trans with ``x*(pow (Rabsolu y) n)``. -Do 2 Rewrite <- (Rmult_sym (pow (Rabsolu y) n)). -Apply Rle_monotony. -Apply pow_le; Apply Rabsolu_pos. -Assumption. -Apply Rle_monotony. -Apply H0. -Apply Hrecn. -Apply Rle_trans with (Rabsolu y); [Apply Rabsolu_pos | Exact H]. -Qed. - (* Dans un espace complet, la convergence normale implique la convergence uniforme *) Lemma CVN_CVU : (fn:nat->R->R;cv:(x:R)(sigTT ? [l:R](Un_cv [N:nat](SP fn N x) l));r:posreal) (CVN_r fn r) -> (CVU [n:nat](SP fn n) (SFL fn cv) ``0`` r). @@ -355,7 +68,7 @@ Qed. Lemma CVU_continuity : (fn:nat->R->R;f:R->R;x:R;r:posreal) (CVU fn f x r) -> ((n:nat)(y:R) (Boule x r y)->(continuity_pt (fn n) y)) -> ((y:R) (Boule x r y) -> (continuity_pt f y)). Intros; Unfold continuity_pt; Unfold continue_in; Unfold limit1_in; Unfold limit_in; Simpl; Unfold R_dist; Intros. Unfold CVU in H. -Cut ``0<eps/3``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_3_0]]. +Cut ``0<eps/3``; [Intro | Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]]. Elim (H ? H3); Intros N0 H4. Assert H5 := (H0 N0 y H1). Cut (EXT del : posreal | (h:R) ``(Rabsolu h)<del`` -> (Boule x r ``y+h``) ). @@ -448,45 +161,6 @@ Apply H1. Unfold Boule; Simpl; Rewrite minus_R0; Pattern 1 (Rabsolu x); Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rlt_R0_R1. Qed. -(* Théorème de comparaison de convergence pour les séries *) -Lemma Rseries_CV_comp : (An,Bn:nat->R) ((n:nat)``0<=(An n)<=(Bn n)``) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 Bn N) l)) -> (sigTT ? [l:R](Un_cv [N:nat](sum_f_R0 An N) l)). -Intros; Apply cv_cauchy_2. -Assert H0 := (cv_cauchy_1 ? X). -Unfold Cauchy_crit_series; Unfold Cauchy_crit. -Intros; Elim (H0 eps H1); Intros. -Exists x; Intros. -Cut (Rle (R_dist (sum_f_R0 An n) (sum_f_R0 An m)) (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m))). -Intro; Apply Rle_lt_trans with (R_dist (sum_f_R0 Bn n) (sum_f_R0 Bn m)). -Assumption. -Apply H2; Assumption. -Assert H5 := (lt_eq_lt_dec n m). -Elim H5; Intro. -Elim a; Intro. -Rewrite (tech2 An n m); [Idtac | Assumption]. -Rewrite (tech2 Bn 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; Repeat Rewrite Rabsolu_right. -Apply sum_Rle; Intros. -Elim (H (plus (S n) n0)); Intros. -Apply H8. -Apply Rle_sym1; Apply cond_pos_sum; Intro. -Elim (H (plus (S n) n0)); Intros. -Apply Rle_trans with (An (plus (S n) n0)); Assumption. -Apply Rle_sym1; Apply cond_pos_sum; Intro. -Elim (H (plus (S n) n0)); Intros; Assumption. -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 Bn 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 Bn m)); Do 2 Rewrite Rplus_assoc; Do 2 Rewrite Rplus_Ropp_l; Do 2 Rewrite Rplus_Or; Repeat Rewrite Rabsolu_right. -Apply sum_Rle; Intros. -Elim (H (plus (S m) n0)); Intros; Apply H8. -Apply Rle_sym1; Apply cond_pos_sum; Intro. -Elim (H (plus (S m) n0)); Intros. -Apply Rle_trans with (An (plus (S m) n0)); Assumption. -Apply Rle_sym1. -Apply cond_pos_sum; Intro. -Elim (H (plus (S m) n0)); Intros; Assumption. -Qed. - (* Grace a la completude de R, on a le lemme suivant *) Lemma CVN_R_CVS : (fn:nat->R->R) (CVN_R fn) -> ((x:R)(sigTT ? [l:R](Un_cv [N:nat](SP fn N x) l))). Intros; Apply R_complet. |