Quelques ameliorations...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2902 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 220 insertions, 652 deletions

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index 10ebfc0c5..0424b55f8 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -34,21 +34,15 @@ Qed.
 
 Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``.
 Intros; Induction N.
-Simpl; Apply H.
-Apply le_n.
-Replace (sum_f_R0 An (S N)) with ``(sum_f_R0 An N)+(An (S N))``.
-Apply gt0_plus_gt0_is_gt0.
-Apply HrecN; Intros; Apply H.
-Apply le_S; Assumption.
-Apply H.
-Apply le_n.
-Reflexivity.
+Simpl; Apply H; Apply le_n.
+Simpl; Apply gt0_plus_gt0_is_gt0.
+Apply HrecN; Intros; Apply H; Apply le_S; Assumption.
+Apply H; Apply le_n.
 Qed.
 
 (* Relation de Chasles *)
 Lemma tech2 : (An:nat->R;m,n:nat) (lt m n) -> (sum_f_R0 An n) == (Rplus (sum_f_R0 An m) (sum_f_R0 [i:nat]``(An (plus (S m) i))`` (minus n (S m)))). 
-Intros.
-Induction n.
+Intros; Induction n.
 Elim (lt_n_O ? H).
 Cut (lt m n)\/m=n.
 Intro; Elim H0; Intro.
@@ -58,71 +52,44 @@ Replace (sum_f_R0 [i:nat](An (plus (S m) i)) (S (minus n (S m)))) with (Rplus (s
 Replace (plus (S m) (S (minus n (S m)))) with (S n).
 Rewrite (Hrecn H1).
 Ring.
-Apply INR_eq.
-Rewrite S_INR.
-Rewrite plus_INR.
-Do 2 Rewrite S_INR.
-Rewrite minus_INR.
-Rewrite S_INR.
-Ring.
+Apply INR_eq; Rewrite S_INR; Rewrite plus_INR; Do 2 Rewrite S_INR; Rewrite minus_INR.
+Rewrite S_INR; Ring.
 Apply lt_le_S; Assumption.
-Apply INR_eq.
-Rewrite S_INR.
-Repeat Rewrite minus_INR.
-Repeat Rewrite S_INR.
-Ring.
-Apply le_n_S.
-Apply lt_le_weak; Assumption.
+Apply INR_eq; Rewrite S_INR; Repeat Rewrite minus_INR.
+Repeat Rewrite S_INR; Ring.
+Apply le_n_S; Apply lt_le_weak; Assumption.
 Apply lt_le_S; Assumption.
-Rewrite H1.
-Replace (minus (S n) (S n)) with O.
-Simpl.
-Replace (plus n O) with n; [Idtac | Ring].
-Reflexivity.
-Apply minus_n_n.
+Rewrite H1; Rewrite <- minus_n_n; Simpl.
+Replace (plus n O) with n; [Reflexivity | Ring].
 Inversion H.
 Right; Reflexivity.
-Left.
-Apply lt_le_trans with (S m).
-Apply lt_n_Sn.
-Assumption.
+Left; Apply lt_le_trans with (S m); [Apply lt_n_Sn | Assumption].
 Qed.
 
 (* Somme d'une suite géométrique *)
 Lemma tech3 : (k:R;N:nat) ``k<>1`` -> (sum_f_R0 [i:nat](pow k i) N)==``(1-(pow k (S N)))/(1-k)``.
-Intros.
-Induction N.
-Simpl.
-Field.
-Replace ``1+ -k`` with ``1-k``; [Idtac | Ring].
-Apply Rminus_eq_contra.
-Apply not_sym.
-Assumption.
-Replace (sum_f_R0 ([i:nat](pow k i)) (S N)) with (Rplus (sum_f_R0 [i:nat](pow k i) N) (pow k (S N))); [Idtac | Reflexivity].
-Rewrite HrecN.
-Replace ``(1-(pow k (S N)))/(1-k)+(pow k (S N))`` with ``((1-(pow k (S N)))+(1-k)*(pow k (S N)))/(1-k)``; [Idtac | Field; Replace ``1+ -k`` with ``1-k``; [Idtac | Ring]; Apply Rminus_eq_contra; Apply not_sym; Assumption].
-Replace ``(1-(pow k (S N))+(1-k)*(pow k (S N)))`` with ``1-k*(pow k (S N))``; [Idtac | Ring].
-Replace (S (S N)) with (plus (1) (S N)).
-Rewrite pow_add.
-Simpl.
-Rewrite Rmult_1r.
+Intros; Cut ``1-k<>0``.
+Intro; Induction N.
+Simpl; Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rinv_r_sym.
 Reflexivity.
-Ring.
+Apply H0.
+Replace (sum_f_R0 ([i:nat](pow k i)) (S N)) with (Rplus (sum_f_R0 [i:nat](pow k i) N) (pow k (S N))); [Idtac | Reflexivity]; Rewrite HrecN; Replace ``(1-(pow k (S N)))/(1-k)+(pow k (S N))`` with ``((1-(pow k (S N)))+(1-k)*(pow k (S N)))/(1-k)``.
+Apply r_Rmult_mult with ``1-k``.
+Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(1-k)``); Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym; [ Do 2 Rewrite Rmult_1l; Simpl; Ring | Apply H0].
+Apply H0.
+Unfold Rdiv; Rewrite Rmult_Rplus_distrl; Rewrite (Rmult_sym ``1-k``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Reflexivity.
+Apply H0.
+Apply Rminus_eq_contra; Red; Intro; Elim H; Symmetry; Assumption.
 Qed.
 
 Lemma tech4 : (An:nat->R;k:R;N:nat) ``0<=k`` -> ((i:nat)``(An (S i))<k*(An i)``) -> ``(An N)<=(An O)*(pow k N)``.
-Intros.
-Induction N.
-Simpl.
-Right; Ring.
+Intros; Induction N.
+Simpl; Right; Ring.
 Apply Rle_trans with ``k*(An N)``.
 Left; Apply (H0 N).
 Replace (S N) with (plus N (1)); [Idtac | Ring].
-Rewrite pow_add.
-Simpl.
-Rewrite Rmult_1r.
-Replace ``(An O)*((pow k N)*k)`` with ``k*((An O)*(pow k N))``; [Idtac | Ring].
-Apply Rle_monotony.
+Rewrite pow_add; Simpl; Rewrite Rmult_1r; Replace ``(An O)*((pow k N)*k)`` with ``k*((An O)*(pow k N))``; [Idtac | Ring]; Apply Rle_monotony.
 Assumption.
 Apply HrecN.
 Qed.
@@ -132,53 +99,35 @@ Intros; Reflexivity.
 Qed.
 
 Lemma tech6 : (An:nat->R;k:R;N:nat) ``0<=k`` -> ((i:nat)``(An (S i))<k*(An i)``) -> (Rle (sum_f_R0 An N) (Rmult (An O) (sum_f_R0 [i:nat](pow k i) N))).
-Intros.
-Induction N.
-Simpl.
-Right; Ring.
+Intros; Induction N.
+Simpl; Right; Ring.
 Apply Rle_trans with (Rplus (Rmult (An O) (sum_f_R0 [i:nat](pow k i) N)) (An (S N))).
-Replace ``(sum_f_R0 An (S N))`` with ``(sum_f_R0 An N)+(An (S N))``.
-Do 2 Rewrite <- (Rplus_sym (An (S N))).
-Apply Rle_compatibility.
+Rewrite tech5; Do 2 Rewrite <- (Rplus_sym (An (S N))); Apply Rle_compatibility.
 Apply HrecN.
-Symmetry; Apply tech5.
-Rewrite tech5.
-Rewrite Rmult_Rplus_distr.
-Apply Rle_compatibility.
+Rewrite tech5 ; Rewrite Rmult_Rplus_distr; Apply Rle_compatibility.
 Apply tech4; Assumption.
 Qed.
 
 Lemma tech7 : (r1,r2:R) ``r1<>0`` -> ``r2<>0`` -> ``r1<>r2`` -> ``/r1<>/r2``.
-Intros.
-Red.
-Intro.
+Intros; Red; Intro.
 Assert H3 := (Rmult_mult_r r1 ? ? H2).
 Rewrite <- Rinv_r_sym in H3; [Idtac | Assumption].
 Assert H4 := (Rmult_mult_r r2 ? ? H3).
-Rewrite Rmult_1r in H4.
-Rewrite <- Rmult_assoc in H4.
+Rewrite Rmult_1r in H4; Rewrite <- Rmult_assoc in H4.
 Rewrite Rinv_r_simpl_m in H4; [Idtac | Assumption].
 Elim H1; Symmetry; Assumption.
 Qed.
 
 Lemma tech8 : (n,i:nat) (le n (plus (S n) i)).
-Intros.
-Induction i.
-Replace (plus (S n) O) with (S n).
-Apply le_n_Sn.
-Ring.
+Intros; Induction i.
+Replace (plus (S n) O) with (S n); [Apply le_n_Sn | Ring].
 Replace (plus (S n) (S i)) with (S (plus (S n) i)).
 Apply le_S; Assumption.
-Cut (m:nat)(S m)=(plus m (1)); [Intro | Intro; Ring].
-Rewrite H.
-Rewrite (H n).
-Rewrite (H i).
-Ring.
+Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
 Qed.
 
 Lemma tech9 : (Un:nat->R) (Un_growing Un) -> ((m,n:nat)(le m n)->``(Un m)<=(Un n)``).
-Intros.
-Unfold Un_growing in H.
+Intros; Unfold Un_growing in H.
 Induction n.
 Induction m.
 Right; Reflexivity.
@@ -195,186 +144,100 @@ Left; Assumption.
 Qed.
 
 Lemma tech10 : (Un:nat->R;x:R) (Un_growing Un) -> (is_lub (EUn Un) x) -> (Un_cv Un x).
-Intros.
-Cut (bound (EUn Un)).
-Intro.
-Assert H2 := (Un_cv_crit ? H H1).
+Intros; Cut (bound (EUn Un)).
+Intro; Assert H2 := (Un_cv_crit ? H H1).
 Elim H2; Intros.
 Case (total_order_T x x0); Intro.
 Elim s; Intro.
 Cut (n:nat)``(Un n)<=x``.
-Intro.
-Unfold Un_cv in H3.
-Cut ``0<x0-x``.
-Intro.
-Elim (H3 ``x0-x`` H5); Intros.
+Intro; Unfold Un_cv in H3; Cut ``0<x0-x``.
+Intro; Elim (H3 ``x0-x`` H5); Intros.
 Cut (ge x1 x1).
-Intro.
-Assert H8 := (H6 x1 H7).
-Unfold R_dist in H8.
-Rewrite Rabsolu_left1 in H8.
-Rewrite Ropp_distr2 in H8.
-Unfold Rminus in H8.
+Intro; Assert H8 := (H6 x1 H7).
+Unfold R_dist in H8; Rewrite Rabsolu_left1 in H8.
+Rewrite Ropp_distr2 in H8; Unfold Rminus in H8.
 Assert H9 := (Rlt_anti_compatibility ``x0`` ? ? H8).
 Assert H10 := (Ropp_Rlt ? ? H9).
 Assert H11 := (H4 x1).
 Elim (Rlt_antirefl ? (Rlt_le_trans ? ? ? H10 H11)).
-Apply Rle_minus.
-Apply Rle_trans with x.
+Apply Rle_minus; Apply Rle_trans with x.
 Apply H4.
 Left; Assumption.
 Unfold ge; Apply le_n.
-Apply Rgt_minus.
-Assumption.
-Intro.
-Unfold is_lub in H0.
-Unfold is_upper_bound in H0.
-Elim H0; Intros.
-Apply H4.
-Unfold EUn.
-Exists n.
-Reflexivity.
+Apply Rgt_minus; Assumption.
+Intro; Unfold is_lub in H0; Unfold is_upper_bound in H0; Elim H0; Intros.
+Apply H4; Unfold EUn; Exists n; Reflexivity.
 Rewrite b; Assumption.
 Cut ((n:nat)``(Un n)<=x0``).
-Intro.
-Unfold is_lub in H0.
-Unfold is_upper_bound in H0.
-Elim H0; Intros.
+Intro; Unfold is_lub in H0; Unfold is_upper_bound in H0; Elim H0; Intros.
 Cut (y:R)(EUn Un y)->``y<=x0``.
-Intro.
-Assert H8 := (H6 ? H7). 
+Intro; Assert H8 := (H6 ? H7). 
 Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H8 r)).
-Unfold EUn.
-Intros.
-Elim H7; Intros.
+Unfold EUn; Intros; Elim H7; Intros.
 Rewrite H8; Apply H4.
-Intro.
-Case (total_order_Rle (Un n) x0); Intro.
+Intro; Case (total_order_Rle (Un n) x0); Intro.
 Assumption.
 Cut (n0:nat)(le n n0) -> ``x0<(Un n0)``. 
-Intro.
-Unfold Un_cv in H3.
-Cut ``0<(Un n)-x0``.
-Intro.
-Elim (H3 ``(Un n)-x0`` H5); Intros.
+Intro; Unfold Un_cv in H3; Cut ``0<(Un n)-x0``.
+Intro; Elim (H3 ``(Un n)-x0`` H5); Intros.
 Cut (ge (max n x1) x1).
-Intro.
-Assert H8 := (H6 (max n x1) H7).
+Intro; Assert H8 := (H6 (max n x1) H7).
 Unfold R_dist in H8.
 Rewrite Rabsolu_right in H8.
 Unfold Rminus in H8; Do 2 Rewrite <- (Rplus_sym ``-x0``) in H8.
 Assert H9 := (Rlt_anti_compatibility ? ? ? H8).
 Cut ``(Un n)<=(Un (max n x1))``.
-Intro.
-Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H10 H9)).
-Apply tech9.
-Assumption.
-Apply le_max_l.
+Intro; Elim (Rlt_antirefl ? (Rle_lt_trans ? ? ? H10 H9)).
+Apply tech9; [Assumption | Apply le_max_l].
 Apply Rge_trans with ``(Un n)-x0``.
-Unfold Rminus; Apply Rle_sym1.
-Do 2 Rewrite <- (Rplus_sym ``-x0``).
-Apply Rle_compatibility.
-Apply tech9.
-Assumption.
-Apply le_max_l.
+Unfold Rminus; Apply Rle_sym1; Do 2 Rewrite <- (Rplus_sym ``-x0``); Apply Rle_compatibility.
+Apply tech9; [Assumption | Apply le_max_l].
 Left; Assumption.
 Unfold ge; Apply le_max_r.
 Apply Rlt_anti_compatibility with x0.
-Rewrite Rplus_Or.
-Unfold Rminus; Rewrite (Rplus_sym x0).
-Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or.
-Apply H4.
-Apply le_n.
-Intros.
-Apply Rlt_le_trans with (Un n).
+Rewrite Rplus_Or; Unfold Rminus; Rewrite (Rplus_sym x0); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply H4; Apply le_n.
+Intros; Apply Rlt_le_trans with (Un n).
 Case (total_order_Rlt_Rle x0 (Un n)); Intro.
 Assumption.
 Elim n0; Assumption.
 Apply tech9; Assumption.
-Unfold bound.
-Exists x.
-Unfold is_lub in H0.
-Elim H0; Intros; Assumption.
+Unfold bound; Exists x; Unfold is_lub in H0; Elim H0; Intros; Assumption.
 Qed.
 
 Lemma tech11 : (An,Bn,Cn:nat->R;N:nat) ((i:nat) (An i)==``(Bn i)-(Cn i)``) -> (sum_f_R0 An N)==``(sum_f_R0 Bn N)-(sum_f_R0 Cn N)``.
-Intros.
-Induction N.
-Simpl.
-Apply H.
-Replace (sum_f_R0 An (S N)) with ``(sum_f_R0 An N)+(An (S N))``; [Idtac | Reflexivity].
-Replace (sum_f_R0 Bn (S N)) with ``(sum_f_R0 Bn N)+(Bn (S N))``; [Idtac | Reflexivity].
-Replace (sum_f_R0 Cn (S N)) with ``(sum_f_R0 Cn N)+(Cn (S N))``; [Idtac | Reflexivity].
-Rewrite HrecN.
-Unfold Rminus.
-Repeat Rewrite Rplus_assoc.
-Apply Rplus_plus_r.
-Rewrite Ropp_distr1.
-Rewrite <- Rplus_assoc.
-Rewrite <- (Rplus_sym ``-(sum_f_R0 Cn N)``).
-Rewrite Rplus_assoc.
-Apply Rplus_plus_r.
-Unfold Rminus in H.
-Apply H.
+Intros; Induction N.
+Simpl; Apply H.
+Do 3 Rewrite tech5; Rewrite HrecN; Rewrite (H (S N)); Ring.
 Qed.
 
 Lemma tech12 : (An:nat->R;x:R;l:R) (Un_cv [N:nat](sum_f_R0 [i:nat]``(An i)*(pow x i)`` N) l) -> (Pser An x l).
-Intros.
-Unfold Pser.
-Unfold infinit_sum.
-Unfold Un_cv in H.
-Assumption.
+Intros; Unfold Pser; Unfold infinit_sum; Unfold Un_cv in H; Assumption.
 Qed. 
 
 Lemma tech13 : (An:nat->R;k:R) ``0<=k<1`` -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) k) -> (EXT k0 : R | ``k<k0<1`` /\ (EX N:nat | (n:nat) (le N n)->``(Rabsolu ((An (S n))/(An n)))<k0``)).
-Intros.
-Exists ``k+(1-k)/2``.
+Intros; Exists ``k+(1-k)/2``.
 Split.
 Split.
-Pattern 1 k; Rewrite <- Rplus_Or.
-Apply Rlt_compatibility.
+Pattern 1 k; Rewrite <- Rplus_Or; Apply Rlt_compatibility.
 Unfold Rdiv; Apply Rmult_lt_pos.
-Apply Rlt_anti_compatibility with k; Rewrite Rplus_Or.
-Replace ``k+(1-k)`` with R1; [Elim H; Intros; Assumption | Ring].
+Apply Rlt_anti_compatibility with k; Rewrite Rplus_Or; Replace ``k+(1-k)`` with R1; [Elim H; Intros; Assumption | Ring].
 Apply Rlt_Rinv; Apply Rgt_2_0.
 Apply Rlt_monotony_contra with ``2``.
 Apply Rgt_2_0.
-Unfold Rdiv.
-Rewrite Rmult_1r.
-Rewrite Rmult_Rplus_distr.
-Pattern 1 ``2``; Rewrite Rmult_sym.
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1r.
-Replace ``2*k+(1-k)`` with ``1+k``; [Idtac | Ring].
+Unfold Rdiv; Rewrite Rmult_1r; Rewrite Rmult_Rplus_distr; Pattern 1 ``2``; Rewrite Rmult_sym; Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1r; Replace ``2*k+(1-k)`` with ``1+k``; [Idtac | Ring].
 Elim H; Intros.
 Apply Rlt_compatibility; Assumption.
-Unfold Un_cv in H0.
-Cut ``0<(1-k)/2``.
-Intro.
-Elim (H0 ``(1-k)/2`` H1); Intros.
-Exists x.
-Intros.
+Unfold Un_cv in H0; Cut ``0<(1-k)/2``.
+Intro; Elim (H0 ``(1-k)/2`` H1); Intros.
+Exists x; Intros.
 Assert H4 := (H2 n H3).
-Unfold R_dist in H4.
-Rewrite <- Rabsolu_Rabsolu.
-Replace ``(Rabsolu ((An (S n))/(An n)))`` with ``((Rabsolu ((An (S n))/(An n)))-k)+k``; [Idtac | Ring].
-Apply Rle_lt_trans with ``(Rabsolu ((Rabsolu ((An (S n))/(An n)))-k))+(Rabsolu k)``.
+Unfold R_dist in H4; Rewrite <- Rabsolu_Rabsolu; Replace ``(Rabsolu ((An (S n))/(An n)))`` with ``((Rabsolu ((An (S n))/(An n)))-k)+k``; [Idtac | Ring]; Apply Rle_lt_trans with ``(Rabsolu ((Rabsolu ((An (S n))/(An n)))-k))+(Rabsolu k)``.
 Apply Rabsolu_triang.
 Rewrite (Rabsolu_right k).
-Apply Rlt_anti_compatibility with ``-k``.
-Rewrite <- (Rplus_sym k).
-Repeat Rewrite <- Rplus_assoc.
-Rewrite Rplus_Ropp_l.
-Repeat Rewrite Rplus_Ol.
-Apply H4.
-Apply Rle_sym1.
-Elim H; Intros; Assumption.
+Apply Rlt_anti_compatibility with ``-k``; Rewrite <- (Rplus_sym k); Repeat Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Repeat Rewrite Rplus_Ol; Apply H4.
+Apply Rle_sym1; Elim H; Intros; Assumption.
 Unfold Rdiv; Apply Rmult_lt_pos.
-Apply Rlt_anti_compatibility with k.
-Rewrite Rplus_Or.
-Elim H; Intros.
-Replace ``k+(1-k)`` with R1; [Assumption | Ring].
+Apply Rlt_anti_compatibility with k; Rewrite Rplus_Or; Elim H; Intros; Replace ``k+(1-k)`` with R1; [Assumption | Ring].
 Apply Rlt_Rinv; Apply Rgt_2_0.
 Qed.
 
@@ -387,125 +250,67 @@ Definition SigT := Specif.sigT.
 Lemma Alembert_positive :  (An:nat->R) ((n:nat)``0<(An n)``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) R0) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
 Intros An H H0.
 Cut (sigTT R [l:R](is_lub (EUn [N:nat](sum_f_R0 An N)) l)) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
-Intro.
-Apply X.
+Intro; Apply X.
 Apply complet.
-2:Exists (sum_f_R0 An O).
-2:Unfold EUn.
-2:Exists O.
-2:Reflexivity.
-Unfold Un_cv in H0.
-Unfold bound.
-Cut ``0</2``; [Intro | Apply Rlt_Rinv; Apply Rgt_2_0].
+Unfold Un_cv in H0; Unfold bound; Cut ``0</2``; [Intro | Apply Rlt_Rinv; Apply Rgt_2_0].
 Elim (H0 ``/2`` H1); Intros.
 Exists ``(sum_f_R0 An x)+2*(An (S x))``.
-Unfold is_upper_bound.
-Intros.
-Unfold EUn in H3.
-Elim H3; Intros.
-Rewrite H4.
-Assert H5 := (lt_eq_lt_dec x1 x).
+Unfold is_upper_bound; Intros; Unfold EUn in H3; Elim H3; Intros.
+Rewrite H4; Assert H5 := (lt_eq_lt_dec x1 x).
 Elim H5; Intros.
 Elim a; Intro.
 Replace (sum_f_R0 An x) with (Rplus (sum_f_R0 An x1) (sum_f_R0 [i:nat](An (plus (S x1) i)) (minus x (S x1)))).
-Pattern 1 (sum_f_R0 An x1); Rewrite <- Rplus_Or.
-Rewrite Rplus_assoc.
-Apply Rle_compatibility.
+Pattern 1 (sum_f_R0 An x1); Rewrite <- Rplus_Or; Rewrite Rplus_assoc; Apply Rle_compatibility.
 Left; Apply gt0_plus_gt0_is_gt0.
-Apply tech1.
-Intros.
-Apply H.
-Apply Rmult_lt_pos.
-Apply Rgt_2_0.
-Apply H.
+Apply tech1; Intros; Apply H.
+Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply H].
 Symmetry; Apply tech2; Assumption.
-Rewrite b.
-Pattern 1 (sum_f_R0 An x); Rewrite <- Rplus_Or.
-Apply Rle_compatibility.
-Left; Apply Rmult_lt_pos.
-Apply Rgt_2_0.
-Apply H.
+Rewrite b; Pattern 1 (sum_f_R0 An x); Rewrite <- Rplus_Or; Apply Rle_compatibility.
+Left; Apply Rmult_lt_pos; [Apply Rgt_2_0 | Apply H].
 Replace (sum_f_R0 An x1) with (Rplus (sum_f_R0 An x) (sum_f_R0 [i:nat](An (plus (S x) i)) (minus x1 (S x)))).
 Apply Rle_compatibility.
-2:Symmetry.
-2:Apply tech2.
-2:Assumption.
 Cut (Rle (sum_f_R0 [i:nat](An (plus (S x) i)) (minus x1 (S x))) (Rmult (An (S x)) (sum_f_R0 [i:nat](pow ``/2`` i) (minus x1 (S x))))).
-Intro.
-Apply Rle_trans with (Rmult (An (S x)) (sum_f_R0 [i:nat](pow ``/2`` i) (minus x1 (S x)))).
+Intro; Apply Rle_trans with (Rmult (An (S x)) (sum_f_R0 [i:nat](pow ``/2`` i) (minus x1 (S x)))).
 Assumption.
-Rewrite <- (Rmult_sym (An (S x))).
-Apply Rle_monotony.
+Rewrite <- (Rmult_sym (An (S x))); Apply Rle_monotony.
 Left; Apply H.
 Rewrite tech3.
 Replace ``1-/2`` with ``/2``.
-Unfold Rdiv.
-Rewrite Rinv_Rinv.
-Pattern 3 ``2``; Rewrite <- Rmult_1r.
-Rewrite <- (Rmult_sym ``2``).
-Apply Rle_monotony.
+Unfold Rdiv; Rewrite Rinv_Rinv.
+Pattern 3 ``2``; Rewrite <- Rmult_1r; Rewrite <- (Rmult_sym ``2``); Apply Rle_monotony.
 Left; Apply Rgt_2_0.
 Left; Apply Rlt_anti_compatibility with ``(pow (/2) (S (minus x1 (S x))))``.
-Replace ``(pow (/2) (S (minus x1 (S x))))+(1-
-   (pow (/2) (S (minus x1 (S x)))))`` with R1; [Idtac | Ring].
-Rewrite <- (Rplus_sym ``1``).
-Pattern 1 R1; Rewrite <- Rplus_Or.
-Apply Rlt_compatibility.
-Apply pow_lt.
-Apply Rlt_Rinv; Apply Rgt_2_0.
+Replace ``(pow (/2) (S (minus x1 (S x))))+(1-(pow (/2) (S (minus x1 (S x)))))`` with R1; [Idtac | Ring].
+Rewrite <- (Rplus_sym ``1``); Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rlt_compatibility.
+Apply pow_lt; Apply Rlt_Rinv; Apply Rgt_2_0.
+DiscrR.
+Apply r_Rmult_mult with ``2``.
+Rewrite Rminus_distr; Rewrite <- Rinv_r_sym.
+Ring.
 DiscrR.
-Field.
 DiscrR.
-Pattern 3 R1; Replace R1 with ``/1``.
-2:Apply Rinv_R1.
-Apply tech7; DiscrR.
+Pattern 3 R1; Replace R1 with ``/1``; [Apply tech7; DiscrR | Apply Rinv_R1].
 Replace (An (S x)) with (An (plus (S x) O)).
 Apply (tech6 [i:nat](An (plus (S x) i)) ``/2``).
 Left; Apply Rlt_Rinv; Apply Rgt_2_0.
-2:Replace (plus (S x) O) with (S x); [Reflexivity | Ring].
-Intro.
-Cut (n:nat)(ge n x)->``(An (S n))</2*(An n)``.
-Intro.
-Replace (plus (S x) (S i)) with (S (plus (S x) i)).
-Apply H6.
-Unfold ge.
-Apply tech8.
-Cut (m:nat)(S m)=(plus m (1)); [Intro | Intro; Ring].
-Rewrite H7.
-Rewrite (H7 x).
-Rewrite (H7 i).
-Ring.
-Intros.
-Unfold R_dist in H2.
-Apply Rlt_monotony_contra with ``/(An n)``.
+Intro; Cut (n:nat)(ge n x)->``(An (S n))</2*(An n)``.
+Intro; Replace (plus (S x) (S i)) with (S (plus (S x) i)).
+Apply H6; Unfold ge; Apply tech8.
+Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
+Intros; Unfold R_dist in H2; Apply Rlt_monotony_contra with ``/(An n)``.
 Apply Rlt_Rinv; Apply H.
-Do 2 Rewrite (Rmult_sym ``/(An n)``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r.
-Replace ``(An (S n))*/(An n)`` with ``(Rabsolu ((Rabsolu ((An (S n))/(An n)))-0))``.
+Do 2 Rewrite (Rmult_sym ``/(An n)``); Rewrite Rmult_assoc; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Replace ``(An (S n))*/(An n)`` with ``(Rabsolu ((Rabsolu ((An (S n))/(An n)))-0))``.
 Apply H2; Assumption.
-Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or.
-Rewrite Rabsolu_Rabsolu.
-Rewrite Rabsolu_right.
+Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu; Rewrite Rabsolu_right.
 Unfold Rdiv; Reflexivity.
-Left; Unfold Rdiv; Change ``0<(An (S n))*/(An n)``; Apply Rmult_lt_pos.
-Apply H.
-Apply Rlt_Rinv; Apply H.
-Red; Intro.
-Assert H8 := (H n).
-Rewrite H7 in H8; Elim (Rlt_antirefl ? H8).
-Intro.
-Elim X; Intros.
-Apply Specif.existT with x.
-Apply tech10.
-2:Assumption.
-Unfold Un_growing.
-Intro.
-Rewrite tech5.
-Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or.
-Apply Rle_compatibility.
-Left; Apply H.
+Left; Unfold Rdiv; Change ``0<(An (S n))*/(An n)``; Apply Rmult_lt_pos; [Apply H | Apply Rlt_Rinv; Apply H].
+Red; Intro; Assert H8 := (H n); Rewrite H7 in H8; Elim (Rlt_antirefl ? H8).
+Replace (plus (S x) O) with (S x); [Reflexivity | Ring].
+Symmetry; Apply tech2; Assumption.
+Exists (sum_f_R0 An O); Unfold EUn; Exists O; Reflexivity.
+Intro; Elim X; Intros.
+Apply Specif.existT with x; Apply tech10; [Unfold Un_growing; Intro; Rewrite tech5; Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply H | Apply p].
 Qed.
 
 Lemma Alembert_general:(An:nat->R) ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) R0) -> (SigT R  [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
@@ -513,387 +318,189 @@ Intros.
 Pose Vn := [i:nat]``(2*(Rabsolu (An i))+(An i))/2``.
 Pose Wn := [i:nat]``(2*(Rabsolu (An i))-(An i))/2``.
 Cut (n:nat)``0<(Vn n)``.
-Intro.
-Cut (n:nat)``0<(Wn n)``.
-Intro.
-Cut (Un_cv [n:nat](Rabsolu ``(Vn (S n))/(Vn n)``) ``0``).
-Intro.
-Cut (Un_cv [n:nat](Rabsolu ``(Wn (S n))/(Wn n)``) ``0``).
-Intro.
-Assert H5 := (Alembert_positive Vn H1 H3).
+Intro; Cut (n:nat)``0<(Wn n)``.
+Intro; Cut (Un_cv [n:nat](Rabsolu ``(Vn (S n))/(Vn n)``) ``0``).
+Intro; Cut (Un_cv [n:nat](Rabsolu ``(Wn (S n))/(Wn n)``) ``0``).
+Intro; Assert H5 := (Alembert_positive Vn H1 H3).
 Assert H6 := (Alembert_positive Wn H2 H4).
 Elim H5; Intros.
 Elim H6; Intros.
-Apply Specif.existT with ``x-x0``.
-Unfold Un_cv.
-Unfold Un_cv in p.
-Unfold Un_cv in p0.
-Intros.
-Cut ``0<eps/2``.
-Intro.
-Elim (p ``eps/2`` H8); Clear p; Intros.
+Apply Specif.existT with ``x-x0``; Unfold Un_cv; Unfold Un_cv in p; Unfold Un_cv in p0; Intros; Cut ``0<eps/2``.
+Intro; Elim (p ``eps/2`` H8); Clear p; Intros.
 Elim (p0 ``eps/2`` H8); Clear p0; Intros.
 Pose N := (max x1 x2).
-Exists N.
-Intros.
-Replace (sum_f_R0 An n) with (Rminus (sum_f_R0 Vn n) (sum_f_R0 Wn n)).
-Unfold R_dist.
-Replace (Rminus (Rminus (sum_f_R0 Vn n) (sum_f_R0 Wn n)) (Rminus x x0)) with (Rplus (Rminus (sum_f_R0 Vn n) x) (Ropp (Rminus (sum_f_R0 Wn n) x0))); [Idtac | Ring].
-Apply Rle_lt_trans with (Rplus (Rabsolu (Rminus (sum_f_R0 Vn n) x)) (Rabsolu (Ropp (Rminus (sum_f_R0 Wn n) x0)))).
+Exists N; Intros; Replace (sum_f_R0 An n) with (Rminus (sum_f_R0 Vn n) (sum_f_R0 Wn n)).
+Unfold R_dist; Replace (Rminus (Rminus (sum_f_R0 Vn n) (sum_f_R0 Wn n)) (Rminus x x0)) with (Rplus (Rminus (sum_f_R0 Vn n) x) (Ropp (Rminus (sum_f_R0 Wn n) x0))); [Idtac | Ring]; Apply Rle_lt_trans with (Rplus (Rabsolu (Rminus (sum_f_R0 Vn n) x)) (Rabsolu (Ropp (Rminus (sum_f_R0 Wn n) x0)))).
 Apply Rabsolu_triang.
-Rewrite Rabsolu_Ropp.
-Apply Rlt_le_trans with ``eps/2+eps/2``.
+Rewrite Rabsolu_Ropp; Apply Rlt_le_trans with ``eps/2+eps/2``.
 Apply Rplus_lt.
-Unfold R_dist in H9.
-Apply H9.
-Unfold ge; Apply le_trans with N.
-Unfold N; Apply le_max_l.
-Assumption.
-Unfold R_dist in H10.
-Apply H10.
-Unfold ge; Apply le_trans with N.
-Unfold N; Apply le_max_r.
-Assumption.
+Unfold R_dist in H9; Apply H9; Unfold ge; Apply le_trans with N; [Unfold N; Apply le_max_l | Assumption].
+Unfold R_dist in H10; Apply H10; Unfold ge; Apply le_trans with N; [Unfold N; Apply le_max_r | Assumption].
 Right; Symmetry; Apply double_var.
-Symmetry; Apply tech11.
-Intro.
-Unfold Vn Wn.
-Field.
+Symmetry; Apply tech11; Intro; Unfold Vn Wn; Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/2``); Apply r_Rmult_mult with ``2``.
+Rewrite Rminus_distr; Repeat Rewrite <- Rmult_assoc; Rewrite <- Rinv_r_sym.
+Ring.
+DiscrR.
 DiscrR.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_2_0].
 Cut (n:nat)``/2*(Rabsolu (An n))<=(Wn n)<=(3*/2)*(Rabsolu (An n))``.
-Intro.
-Cut (n:nat)``/(Wn n)<=2*/(Rabsolu (An n))``.
-Intro.
-Cut (n:nat)``(Wn (S n))/(Wn n)<=3*(Rabsolu (An (S n))/(An n))``.
-Intro.
-Unfold Un_cv.
-Intros.
-Unfold Un_cv in H0.
-Cut ``0<eps/3``.
-Intro.
-Elim (H0 ``eps/3`` H8); Intros.
-Exists x.
-Intros.
+Intro; Cut (n:nat)``/(Wn n)<=2*/(Rabsolu (An n))``.
+Intro; Cut (n:nat)``(Wn (S n))/(Wn n)<=3*(Rabsolu (An (S n))/(An n))``.
+Intro; Unfold Un_cv; Intros; Unfold Un_cv in H0; Cut ``0<eps/3``.
+Intro; Elim (H0 ``eps/3`` H8); Intros.
+Exists x; Intros.
 Assert H11 := (H9 n H10).
-Unfold R_dist.
-Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu.
-Unfold R_dist in H11; Unfold Rminus in H11; Rewrite Ropp_O in H11; Rewrite Rplus_Or in H11; Rewrite Rabsolu_Rabsolu in H11.
-Rewrite Rabsolu_right.
+Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu; Unfold R_dist in H11; Unfold Rminus in H11; Rewrite Ropp_O in H11; Rewrite Rplus_Or in H11; Rewrite Rabsolu_Rabsolu in H11; Rewrite Rabsolu_right.
 Apply Rle_lt_trans with ``3*(Rabsolu ((An (S n))/(An n)))``.
 Apply H6.
 Apply Rlt_monotony_contra with ``/3``.
 Apply Rlt_Rinv; Apply Rgt_3_0.
-Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1l.
-Rewrite <- (Rmult_sym eps).
-Unfold Rdiv in H11; Exact H11.
+Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps); Unfold Rdiv in H11; Exact H11.
 Left; Change ``0<(Wn (S n))/(Wn n)``; Unfold Rdiv; Apply Rmult_lt_pos.
 Apply H2.
 Apply Rlt_Rinv; Apply H2.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_3_0].
-Intro.
-Unfold Rdiv.
-Rewrite Rabsolu_mult.
-Rewrite <- Rmult_assoc.
-Replace ``3`` with ``2*(3*/2)``; [Idtac | Field; DiscrR].
-Apply Rle_trans with ``(Wn (S n))*2*/(Rabsolu (An n))``.
-Rewrite Rmult_assoc.
-Apply Rle_monotony.
+Intro; Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite <- Rmult_assoc; Replace ``3`` with ``2*(3*/2)``; [Idtac | Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; DiscrR]; Apply Rle_trans with ``(Wn (S n))*2*/(Rabsolu (An n))``.
+Rewrite Rmult_assoc; Apply Rle_monotony.
 Left; Apply H2.
 Apply H5.
 Rewrite Rabsolu_Rinv.
-Replace ``(Wn (S n))*2*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*(Wn (S n))``; [Idtac | Ring].
-Replace ``2*(3*/2)*(Rabsolu (An (S n)))*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*((3*/2)*(Rabsolu (An (S n))))``; [Idtac | Ring].
-Apply Rle_monotony.
+Replace ``(Wn (S n))*2*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*(Wn (S n))``; [Idtac | Ring]; Replace ``2*(3*/2)*(Rabsolu (An (S n)))*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*((3*/2)*(Rabsolu (An (S n))))``; [Idtac | Ring]; Apply Rle_monotony.
 Left; Apply Rmult_lt_pos.
 Apply Rgt_2_0.
 Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply H.
 Elim (H4 (S n)); Intros; Assumption.
 Apply H.
-Intro.
-Apply Rle_monotony_contra with (Wn n).
+Intro; Apply Rle_monotony_contra with (Wn n).
 Apply H2.
 Rewrite <- Rinv_r_sym.
 Apply Rle_monotony_contra with (Rabsolu (An n)).
 Apply Rabsolu_pos_lt; Apply H.
-Rewrite Rmult_1r.
-Replace ``(Rabsolu (An n))*((Wn n)*(2*/(Rabsolu (An n))))`` with ``2*(Wn n)*((Rabsolu (An n))*/(Rabsolu (An n)))``; [Idtac | Ring].
-Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r.
-Apply Rle_monotony_contra with ``/2``.
+Rewrite Rmult_1r; Replace ``(Rabsolu (An n))*((Wn n)*(2*/(Rabsolu (An n))))`` with ``2*(Wn n)*((Rabsolu (An n))*/(Rabsolu (An n)))``; [Idtac | Ring]; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Apply Rle_monotony_contra with ``/2``.
 Apply Rlt_Rinv; Apply Rgt_2_0.
-Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_l_sym.
+Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l; Elim (H4 n); Intros; Assumption.
 DiscrR.
 Apply Rabsolu_no_R0; Apply H.
 Red; Intro; Assert H6 := (H2 n); Rewrite H5 in H6; Elim (Rlt_antirefl ? H6).
-Intro.
-Split.
-Unfold Wn.
-Unfold Rdiv.
-Rewrite <- (Rmult_sym ``/2``).
-Apply Rle_monotony.
+Intro; Split.
+Unfold Wn; Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Apply Rle_monotony.
 Left; Apply Rlt_Rinv; Apply Rgt_2_0.
-Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or.
-Rewrite double.
-Unfold Rminus.
-Rewrite Rplus_assoc.
-Apply Rle_compatibility.
+Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Rewrite double; Unfold Rminus; Rewrite Rplus_assoc; Apply Rle_compatibility.
 Apply Rle_anti_compatibility with (An n).
-Rewrite Rplus_Or.
-Rewrite (Rplus_sym (An n)).
-Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or.
-Apply Rle_Rabsolu.
-Unfold Wn.
-Unfold Rdiv.
-Repeat Rewrite <- (Rmult_sym ``/2``).
-Repeat Rewrite Rmult_assoc.
-Apply Rle_monotony.
+Rewrite Rplus_Or; Rewrite (Rplus_sym (An n)); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply Rle_Rabsolu.
+Unfold Wn; Unfold Rdiv; Repeat Rewrite <- (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony.
 Left; Apply Rlt_Rinv; Apply Rgt_2_0.
-Unfold Rminus.
-Rewrite double.
-Replace ``3*(Rabsolu (An n))`` with ``(Rabsolu (An n))+(Rabsolu (An n))+(Rabsolu (An n))``; [Idtac | Ring].
-Repeat Rewrite Rplus_assoc.
-Repeat Apply Rle_compatibility.
-Rewrite <- Rabsolu_Ropp.
-Apply Rle_Rabsolu.
+Unfold Rminus; Rewrite double; Replace ``3*(Rabsolu (An n))`` with ``(Rabsolu (An n))+(Rabsolu (An n))+(Rabsolu (An n))``; [Idtac | Ring]; Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility.
+Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu.
 Cut (n:nat)``/2*(Rabsolu (An n))<=(Vn n)<=(3*/2)*(Rabsolu (An n))``.
-Intro.
-Cut (n:nat)``/(Vn n)<=2*/(Rabsolu (An n))``.
-Intro.
-Cut (n:nat)``(Vn (S n))/(Vn n)<=3*(Rabsolu (An (S n))/(An n))``.
-Intro.
-Unfold Un_cv.
-Intros.
-Unfold Un_cv in H1.
-Cut ``0<eps/3``.
-Intro.
-Elim (H0 ``eps/3`` H7); Intros.
-Exists x.
-Intros.
+Intro; Cut (n:nat)``/(Vn n)<=2*/(Rabsolu (An n))``.
+Intro; Cut (n:nat)``(Vn (S n))/(Vn n)<=3*(Rabsolu (An (S n))/(An n))``.
+Intro; Unfold Un_cv; Intros; Unfold Un_cv in H1; Cut ``0<eps/3``.
+Intro; Elim (H0 ``eps/3`` H7); Intros.
+Exists x; Intros.
 Assert H10 := (H8 n H9).
-Unfold R_dist.
-Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu.
-Unfold R_dist in H10; Unfold Rminus in H10; Rewrite Ropp_O in H10; Rewrite Rplus_Or in H10; Rewrite Rabsolu_Rabsolu in H10.
-Rewrite Rabsolu_right.
+Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu; Unfold R_dist in H10; Unfold Rminus in H10; Rewrite Ropp_O in H10; Rewrite Rplus_Or in H10; Rewrite Rabsolu_Rabsolu in H10; Rewrite Rabsolu_right.
 Apply Rle_lt_trans with ``3*(Rabsolu ((An (S n))/(An n)))``.
 Apply H5.
 Apply Rlt_monotony_contra with ``/3``.
 Apply Rlt_Rinv; Apply Rgt_3_0.
-Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_l_sym; [Idtac | DiscrR].
-Rewrite Rmult_1l.
-Rewrite <- (Rmult_sym eps).
-Unfold Rdiv in H10; Exact H10.
+Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym; [Idtac | DiscrR]; Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps); Unfold Rdiv in H10; Exact H10.
 Left; Change ``0<(Vn (S n))/(Vn n)``; Unfold Rdiv; Apply Rmult_lt_pos.
 Apply H1.
 Apply Rlt_Rinv; Apply H1.
 Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rgt_3_0].
-Intro.
-Unfold Rdiv.
-Rewrite Rabsolu_mult.
-Rewrite <- Rmult_assoc.
-Replace ``3`` with ``2*(3*/2)``; [Idtac | Field; DiscrR].
-Apply Rle_trans with ``(Vn (S n))*2*/(Rabsolu (An n))``.
-Rewrite Rmult_assoc.
-Apply Rle_monotony.
+Intro; Unfold Rdiv; Rewrite Rabsolu_mult; Rewrite <- Rmult_assoc; Replace ``3`` with ``2*(3*/2)``; [Idtac | Rewrite <- Rmult_assoc; Apply Rinv_r_simpl_m; DiscrR]; Apply Rle_trans with ``(Vn (S n))*2*/(Rabsolu (An n))``.
+Rewrite Rmult_assoc; Apply Rle_monotony.
 Left; Apply H1.
 Apply H4.
 Rewrite Rabsolu_Rinv.
-Replace ``(Vn (S n))*2*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*(Vn (S n))``; [Idtac | Ring].
-Replace ``2*(3*/2)*(Rabsolu (An (S n)))*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*((3*/2)*(Rabsolu (An (S n))))``; [Idtac | Ring].
-Apply Rle_monotony.
+Replace ``(Vn (S n))*2*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*(Vn (S n))``; [Idtac | Ring]; Replace ``2*(3*/2)*(Rabsolu (An (S n)))*/(Rabsolu (An n))`` with ``(2*/(Rabsolu (An n)))*((3*/2)*(Rabsolu (An (S n))))``; [Idtac | Ring]; Apply Rle_monotony.
 Left; Apply Rmult_lt_pos.
 Apply Rgt_2_0.
 Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Apply H.
 Elim (H3 (S n)); Intros; Assumption.
 Apply H.
-Intro.
-Apply Rle_monotony_contra with (Vn n).
+Intro; Apply Rle_monotony_contra with (Vn n).
 Apply H1.
 Rewrite <- Rinv_r_sym.
 Apply Rle_monotony_contra with (Rabsolu (An n)).
 Apply Rabsolu_pos_lt; Apply H.
-Rewrite Rmult_1r.
-Replace ``(Rabsolu (An n))*((Vn n)*(2*/(Rabsolu (An n))))`` with ``2*(Vn n)*((Rabsolu (An n))*/(Rabsolu (An n)))``; [Idtac | Ring].
-Rewrite <- Rinv_r_sym.
-Rewrite Rmult_1r.
-Apply Rle_monotony_contra with ``/2``.
+Rewrite Rmult_1r; Replace ``(Rabsolu (An n))*((Vn n)*(2*/(Rabsolu (An n))))`` with ``2*(Vn n)*((Rabsolu (An n))*/(Rabsolu (An n)))``; [Idtac | Ring]; Rewrite <- Rinv_r_sym.
+Rewrite Rmult_1r; Apply Rle_monotony_contra with ``/2``.
 Apply Rlt_Rinv; Apply Rgt_2_0.
-Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_l_sym.
+Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l; Elim (H3 n); Intros; Assumption.
 DiscrR.
 Apply Rabsolu_no_R0; Apply H.
 Red; Intro; Assert H5 := (H1 n); Rewrite H4 in H5; Elim (Rlt_antirefl ? H5).
-Intro.
-Split.
-Unfold Vn.
-Unfold Rdiv.
-Rewrite <- (Rmult_sym ``/2``).
-Apply Rle_monotony.
+Intro; Split.
+Unfold Vn; Unfold Rdiv; Rewrite <- (Rmult_sym ``/2``); Apply Rle_monotony.
 Left; Apply Rlt_Rinv; Apply Rgt_2_0.
-Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or.
-Rewrite double.
-Rewrite Rplus_assoc.
-Apply Rle_compatibility.
-Apply Rle_anti_compatibility with ``-(An n)``.
-Rewrite Rplus_Or.
-Rewrite <- (Rplus_sym (An n)).
-Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol.
-Rewrite <- Rabsolu_Ropp.
-Apply Rle_Rabsolu.
-Unfold Vn.
-Unfold Rdiv.
-Repeat Rewrite <- (Rmult_sym ``/2``).
-Repeat Rewrite Rmult_assoc.
-Apply Rle_monotony.
+Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Rewrite double; Rewrite Rplus_assoc; Apply Rle_compatibility.
+Apply Rle_anti_compatibility with ``-(An n)``; Rewrite Rplus_Or; Rewrite <- (Rplus_sym (An n)); Rewrite <- Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Ol; Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu.
+Unfold Vn; Unfold Rdiv; Repeat Rewrite <- (Rmult_sym ``/2``); Repeat Rewrite Rmult_assoc; Apply Rle_monotony.
 Left; Apply Rlt_Rinv; Apply Rgt_2_0.
-Unfold Rminus.
-Rewrite double.
-Replace ``3*(Rabsolu (An n))`` with ``(Rabsolu (An n))+(Rabsolu (An n))+(Rabsolu (An n))``; [Idtac | Ring].
-Repeat Rewrite Rplus_assoc.
-Repeat Apply Rle_compatibility.
-Apply Rle_Rabsolu.
-Intro.
-Unfold Wn.
-Unfold Rdiv.
-Rewrite <- (Rmult_Or ``/2``).
-Rewrite <- (Rmult_sym ``/2``).
-Apply Rlt_monotony.
+Unfold Rminus; Rewrite double; Replace ``3*(Rabsolu (An n))`` with ``(Rabsolu (An n))+(Rabsolu (An n))+(Rabsolu (An n))``; [Idtac | Ring]; Repeat Rewrite Rplus_assoc; Repeat Apply Rle_compatibility; Apply Rle_Rabsolu.
+Intro; Unfold Wn; Unfold Rdiv; Rewrite <- (Rmult_Or ``/2``); Rewrite <- (Rmult_sym ``/2``); Apply Rlt_monotony.
 Apply Rlt_Rinv; Apply Rgt_2_0.
-Apply Rlt_anti_compatibility with (An n).
-Rewrite Rplus_Or.
-Unfold Rminus.
-Rewrite (Rplus_sym (An n)).
-Rewrite Rplus_assoc.
-Rewrite Rplus_Ropp_l; Rewrite Rplus_Or.
-Apply Rle_lt_trans with (Rabsolu (An n)).
+Apply Rlt_anti_compatibility with (An n); Rewrite Rplus_Or; Unfold Rminus; Rewrite (Rplus_sym (An n)); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_l; Rewrite Rplus_Or; Apply Rle_lt_trans with (Rabsolu (An n)).
 Apply Rle_Rabsolu.
-Rewrite double.
-Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or.
-Apply Rlt_compatibility.
-Apply Rabsolu_pos_lt; Apply H.
-Intro.
-Unfold Vn.
-Unfold Rdiv.
-Rewrite <- (Rmult_Or ``/2``).
-Rewrite <- (Rmult_sym ``/2``).
-Apply Rlt_monotony.
+Rewrite double; Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rabsolu_pos_lt; Apply H.
+Intro; Unfold Vn; Unfold Rdiv; Rewrite <- (Rmult_Or ``/2``); Rewrite <- (Rmult_sym ``/2``); Apply Rlt_monotony.
 Apply Rlt_Rinv; Apply Rgt_2_0.
-Apply Rlt_anti_compatibility with ``-(An n)``.
-Rewrite Rplus_Or.
-Unfold Rminus.
-Rewrite (Rplus_sym ``-(An n)``).
-Rewrite Rplus_assoc.
-Rewrite Rplus_Ropp_r; Rewrite Rplus_Or.
-Apply Rle_lt_trans with (Rabsolu (An n)).
-Rewrite <- Rabsolu_Ropp.
-Apply Rle_Rabsolu.
-Rewrite double.
-Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or.
-Apply Rlt_compatibility.
-Apply Rabsolu_pos_lt; Apply H.
+Apply Rlt_anti_compatibility with ``-(An n)``; Rewrite Rplus_Or; Unfold Rminus; Rewrite (Rplus_sym ``-(An n)``); Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Apply Rle_lt_trans with (Rabsolu (An n)).
+Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu.
+Rewrite double; Pattern 1 (Rabsolu (An n)); Rewrite <- Rplus_Or; Apply Rlt_compatibility; Apply Rabsolu_pos_lt; Apply H.
 Qed.
 
 Lemma Alembert_step1 : (An:nat->R;x:R) ``x<>0`` -> ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) ``0``) -> (SigT R [l:R](Pser An x l)).
-Intros.
-Pose Bn := [i:nat]``(An i)*(pow x i)``.
+Intros; Pose Bn := [i:nat]``(An i)*(pow x i)``.
 Cut (n:nat)``(Bn n)<>0``.
-Intro.
-Cut (Un_cv [n:nat](Rabsolu ``(Bn (S n))/(Bn n)``) ``0``).
-Intro.
-Assert H4 := (Alembert_general Bn H2 H3).
+Intro; Cut (Un_cv [n:nat](Rabsolu ``(Bn (S n))/(Bn n)``) ``0``).
+Intro; Assert H4 := (Alembert_general Bn H2 H3).
 Elim H4; Intros.
-Apply Specif.existT with x0.
-Unfold Bn in p.
-Apply tech12. 
-Assumption.
-Unfold Un_cv.
-Intros.
-Unfold Un_cv in H1.
-Cut ``0<eps/(Rabsolu x)``.
-Intro.
-Elim (H1 ``eps/(Rabsolu x)`` H4); Intros.
-Exists x0.
-Intros.
-Unfold R_dist.
-Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu.
-Unfold Bn.
-Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``.
-Rewrite Rabsolu_mult.
-Apply Rlt_monotony_contra with ``/(Rabsolu x)``.
+Apply Specif.existT with x0; Unfold Bn in p; Apply tech12; Assumption.
+Unfold Un_cv; Intros; Unfold Un_cv in H1; Cut ``0<eps/(Rabsolu x)``.
+Intro; Elim (H1 ``eps/(Rabsolu x)`` H4); Intros.
+Exists x0; Intros; Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu; Unfold Bn; Replace ``((An (S n))*(pow x (S n)))/((An n)*(pow x n))`` with ``(An (S n))/(An n)*x``.
+Rewrite Rabsolu_mult; Apply Rlt_monotony_contra with ``/(Rabsolu x)``.
 Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption.
-Rewrite <- (Rmult_sym (Rabsolu x)).
-Rewrite <- Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1l.
-Rewrite <- (Rmult_sym eps).
-Unfold Rdiv in H5.
-Replace ``(Rabsolu ((An (S n))/(An n)))`` with ``(R_dist (Rabsolu ((An (S n))*/(An n))) 0)``.
+Rewrite <- (Rmult_sym (Rabsolu x)); Rewrite <- Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1l; Rewrite <- (Rmult_sym eps); Unfold Rdiv in H5; Replace ``(Rabsolu ((An (S n))/(An n)))`` with ``(R_dist (Rabsolu ((An (S n))*/(An n))) 0)``.
 Apply H5; Assumption.
-Unfold R_dist.
-Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu.
-Unfold Rdiv; Reflexivity.
+Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Rewrite Rabsolu_Rabsolu; Unfold Rdiv; Reflexivity.
 Apply Rabsolu_no_R0; Assumption.
-Replace (S n) with (plus n (1)); [Idtac | Ring].
-Rewrite pow_add.
-Unfold Rdiv.
-Rewrite Rinv_Rmult.
-Replace ``(An (plus n (S O)))*((pow x n)*(pow x (S O)))*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*(pow x (S O))*/(An n)*((pow x n)*/(pow x n))``; [Idtac | Ring].
-Rewrite <- Rinv_r_sym.
-Simpl.
-Ring.
+Replace (S n) with (plus n (1)); [Idtac | Ring]; Rewrite pow_add; Unfold Rdiv; Rewrite Rinv_Rmult.
+Replace ``(An (plus n (S O)))*((pow x n)*(pow x (S O)))*(/(An n)*/(pow x n))`` with ``(An (plus n (S O)))*(pow x (S O))*/(An n)*((pow x n)*/(pow x n))``; [Idtac | Ring]; Rewrite <- Rinv_r_sym.
+Simpl; Ring.
 Apply pow_nonzero; Assumption.
 Apply H0.
 Apply pow_nonzero; Assumption.
-Unfold Rdiv; Apply Rmult_lt_pos.
-Assumption.
-Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption.
-Intro.
-Unfold Bn.
-Apply prod_neq_R0.
-Apply H0.
-Apply pow_nonzero; Assumption.
+Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Apply Rabsolu_pos_lt; Assumption].
+Intro; Unfold Bn; Apply prod_neq_R0; [Apply H0 | Apply pow_nonzero; Assumption].
 Qed.
 
 Lemma Alembert_step2 : (An:nat->R;x:R) ``x==0`` -> (SigT R [l:R](Pser An x l)).
-Intros.
-Apply Specif.existT with (An O).
-Unfold Pser.
-Unfold infinit_sum.
-Intros.
-Exists O.
-Intros.
-Replace (sum_f_R0 [n0:nat]``(An n0)*(pow x n0)`` n) with (An O).
+Intros; Apply Specif.existT with (An O).
+Unfold Pser; Unfold infinit_sum; Intros; Exists O; Intros; Replace (sum_f_R0 [n0:nat]``(An n0)*(pow x n0)`` n) with (An O).
 Unfold R_dist; Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rabsolu_R0; Assumption.
 Induction n.
-Simpl.
-Ring.
-Rewrite tech5.
-Rewrite Hrecn.
-Rewrite H.
-Simpl.
-Ring.
-Unfold ge; Apply le_O_n.
+Simpl; Ring.
+Rewrite tech5; Rewrite Hrecn; [Rewrite H; Simpl; Ring | Unfold ge; Apply le_O_n].
 Qed.
 
 (* Un critère utile de convergence des séries entières *)
 Theorem Alembert : (An:nat->R;x:R) ((n:nat)``(An n)<>0``) -> (Un_cv [n:nat](Rabsolu ``(An (S n))/(An n)``) ``0``) -> (SigT R [l:R](Pser An x l)).
-Intros.
-Case (total_order_T x R0); Intro.
+Intros; Case (total_order_T x R0); Intro.
 Elim s; Intro.
 Cut ``x<>0``.
-Intro.
-Apply Alembert_step1; Assumption.
+Intro; Apply Alembert_step1; Assumption.
 Red; Intro; Rewrite H1 in a; Elim (Rlt_antirefl ? a).
 Apply Alembert_step2; Assumption.
 Cut ``x<>0``.
-Intro.
-Apply Alembert_step1; Assumption.
+Intro; Apply Alembert_step1; Assumption.
 Red; Intro; Rewrite H1 in r; Elim (Rlt_antirefl ? r).
 Qed.
 
@@ -901,22 +508,14 @@ Qed.
 Lemma Alembert_strong_positive : (An:nat->R;k:R) ``0<=k<1`` -> ((n:nat)``0<(An n)``) -> (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 An k Hyp H H0.
 Cut (sigTT R [l:R](is_lub (EUn [N:nat](sum_f_R0 An N)) l)) -> (SigT R [l:R](Un_cv [N:nat](sum_f_R0 An N) l)).
-Intro.
-Apply X.
+Intro; Apply X.
 Apply complet.
-2:Exists (sum_f_R0 An O).
-2:Unfold EUn.
-2:Exists O.
-2:Reflexivity.
 Assert H1 := (tech13 ? ? Hyp H0).
 Elim H1; Intros.
 Elim H2; Intros.
 Elim H4; Intros.
-Unfold bound.
-Exists ``(sum_f_R0 An x0)+/(1-x)*(An (S x0))``.
-Unfold is_upper_bound.
-Intros.
-Unfold EUn in H6.
+Unfold bound; Exists ``(sum_f_R0 An x0)+/(1-x)*(An (S x0))``.
+Unfold is_upper_bound; Intros; Unfold EUn in H6.
 Elim H6; Intros.
 Rewrite H7.
 Assert H8 := (lt_eq_lt_dec x2 x0).
@@ -924,54 +523,34 @@ Elim H8; Intros.
 Elim a; Intro.
 Replace (sum_f_R0 An x0) with (Rplus (sum_f_R0 An x2) (sum_f_R0 [i:nat](An (plus (S x2) i)) (minus x0 (S x2)))).
 Pattern 1 (sum_f_R0 An x2); Rewrite <- Rplus_Or.
-Rewrite Rplus_assoc.
-Apply Rle_compatibility.
+Rewrite Rplus_assoc; Apply Rle_compatibility.
 Left; Apply gt0_plus_gt0_is_gt0.
 Apply tech1.
-Intros.
-Apply H.
+Intros; Apply H.
 Apply Rmult_lt_pos.
-Apply Rlt_Rinv.
-Apply Rlt_anti_compatibility with x.
-Rewrite Rplus_Or.
-Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring].
+Apply Rlt_Rinv; Apply Rlt_anti_compatibility with x; Rewrite Rplus_Or; Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring].
 Apply H.
 Symmetry; Apply tech2; Assumption.
-Rewrite b.
-Pattern 1 (sum_f_R0 An x0); Rewrite <- Rplus_Or.
-Apply Rle_compatibility.
+Rewrite b; Pattern 1 (sum_f_R0 An x0); Rewrite <- Rplus_Or; Apply Rle_compatibility.
 Left; Apply Rmult_lt_pos.
-Apply Rlt_Rinv.
-Apply Rlt_anti_compatibility with x.
-Rewrite Rplus_Or.
-Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring].
+Apply Rlt_Rinv; Apply Rlt_anti_compatibility with x; Rewrite Rplus_Or; Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring].
 Apply H.
 Replace (sum_f_R0 An x2) with (Rplus (sum_f_R0 An x0) (sum_f_R0 [i:nat](An (plus (S x0) i)) (minus x2 (S x0)))).
 Apply Rle_compatibility.
-2:Symmetry.
-2:Apply tech2.
-2:Assumption.
 Cut (Rle (sum_f_R0 [i:nat](An (plus (S x0) i)) (minus x2 (S x0))) (Rmult (An (S x0)) (sum_f_R0 [i:nat](pow x i) (minus x2 (S x0))))).
-Intro.
-Apply Rle_trans with (Rmult (An (S x0)) (sum_f_R0 [i:nat](pow x i) (minus x2 (S x0)))).
+Intro; Apply Rle_trans with (Rmult (An (S x0)) (sum_f_R0 [i:nat](pow x i) (minus x2 (S x0)))).
 Assumption.
-Rewrite <- (Rmult_sym (An (S x0))).
-Apply Rle_monotony.
+Rewrite <- (Rmult_sym (An (S x0))); Apply Rle_monotony.
 Left; Apply H.
 Rewrite tech3.
-Unfold Rdiv.
-Apply Rle_monotony_contra with ``1-x``.
+Unfold Rdiv; Apply Rle_monotony_contra with ``1-x``.
 Apply Rlt_anti_compatibility with x; Rewrite Rplus_Or.
 Replace ``x+(1-x)`` with R1; [Elim H3; Intros; Assumption | Ring].
 Do 2 Rewrite (Rmult_sym ``1-x``).
-Rewrite Rmult_assoc.
-Rewrite <- Rinv_l_sym.
-Rewrite Rmult_1r.
-Apply Rle_anti_compatibility with ``(pow x (S (minus x2 (S x0))))``.
+Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
+Rewrite Rmult_1r; Apply Rle_anti_compatibility with ``(pow x (S (minus x2 (S x0))))``.
 Replace ``(pow x (S (minus x2 (S x0))))+(1-(pow x (S (minus x2 (S x0)))))`` with R1; [Idtac | Ring].
-Rewrite <- (Rplus_sym R1).
-Pattern 1 R1; Rewrite <- Rplus_Or.
-Apply Rle_compatibility.
+Rewrite <- (Rplus_sym R1); Pattern 1 R1; Rewrite <- Rplus_Or; Apply Rle_compatibility.
 Left; Apply pow_lt.
 Apply Rle_lt_trans with k.
 Elim Hyp; Intros; Assumption.
@@ -988,7 +567,6 @@ Apply (tech6 [i:nat](An (plus (S x0) i)) x).
 Left; Apply Rle_lt_trans with k.
 Elim Hyp; Intros; Assumption.
 Elim H3; Intros; Assumption.
-2:Replace (plus (S x0) O) with (S x0); [Reflexivity | Ring].
 Intro.
 Cut (n:nat)(ge n x0)->``(An (S n))<x*(An n)``.
 Intro.
@@ -996,11 +574,7 @@ Replace (plus (S x0) (S i)) with (S (plus (S x0) i)).
 Apply H9.
 Unfold ge.
 Apply tech8.
-Cut (m:nat)(S m)=(plus m (1)); [Intro | Intro; Ring].
-Rewrite H10.
-Rewrite (H10 x0).
-Rewrite (H10 i).
-Ring.
+  Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring.
 Intros.
 Apply Rlt_monotony_contra with ``/(An n)``.
 Apply Rlt_Rinv; Apply H.
@@ -1018,15 +592,9 @@ Apply Rlt_Rinv; Apply H.
 Red; Intro.
 Assert H11 := (H n).
 Rewrite H10 in H11; Elim (Rlt_antirefl ? H11).
-Intro.
-Elim X; Intros.
-Apply Specif.existT with x.
-Apply tech10.
-2:Assumption.
-Unfold Un_growing.
-Intro.
-Rewrite tech5.
-Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or.
-Apply Rle_compatibility.
-Left; Apply H.
+Replace (plus (S x0) O) with (S x0); [Reflexivity | Ring].
+Symmetry; Apply tech2; Assumption.
+Exists (sum_f_R0 An O); Unfold EUn; Exists O; Reflexivity.
+Intro; Elim X; Intros.
+Apply Specif.existT with x; Apply tech10; [Unfold Un_growing; Intro; Rewrite tech5; Pattern 1 (sum_f_R0 An n); Rewrite <- Rplus_Or; Apply Rle_compatibility; Left; Apply H | Apply p].
 Qed.