Removed redundant and ill-named technical lemma.

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

1 files changed, 0 insertions, 67 deletions

diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index e53e9cc6d..82647c837 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -848,73 +848,6 @@ Proof.
   left; assumption.
 Qed.
 
-Lemma tech10 :
-  forall (Un:nat -> R) (x:R), Un_growing Un -> is_lub (EUn Un) x -> Un_cv Un x.
-Proof.
-  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 (forall n:nat, Un n <= x).
-  intro; unfold Un_cv in H3; cut (0 < x0 - x).
-  intro; elim (H3 (x0 - x) H5); intros.
-  cut (x1 >= x1)%nat.
-  intro; assert (H8 := H6 x1 H7).
-  unfold R_dist in H8; rewrite Rabs_left1 in H8.
-  rewrite Ropp_minus_distr in H8; unfold Rminus in H8.
-  assert (H9 := Rplus_lt_reg_r x0 _ _ H8).
-  assert (H10 := Ropp_lt_cancel _ _ H9).
-  assert (H11 := H4 x1).
-  elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H10 H11)).
-  apply Rle_minus; apply Rle_trans with x.
-  apply H4.
-  left; assumption.
-  unfold ge in |- *; 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 in |- *; exists n; reflexivity.
-  rewrite b; assumption.
-  cut (forall n:nat, Un n <= x0).
-  intro; unfold is_lub in H0; unfold is_upper_bound in H0; elim H0; intros.
-  cut (forall y:R, EUn Un y -> y <= x0).
-  intro; assert (H8 := H6 _ H7).
-  elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H8 r)).
-  unfold EUn in |- *; intros; elim H7; intros.
-  rewrite H8; apply H4.
-  intro; case (Rle_dec (Un n) x0); intro.
-  assumption.
-  cut (forall n0:nat, (n <= n0)%nat -> x0 < Un n0).
-  intro; unfold Un_cv in H3; cut (0 < Un n - x0).
-  intro; elim (H3 (Un n - x0) H5); intros.
-  cut (max n x1 >= x1)%nat.
-  intro; assert (H8 := H6 (max n x1) H7).
-  unfold R_dist in H8.
-  rewrite Rabs_right in H8.
-  unfold Rminus in H8; do 2 rewrite <- (Rplus_comm (- x0)) in H8.
-  assert (H9 := Rplus_lt_reg_r _ _ _ H8).
-  cut (Un n <= Un (max n x1)).
-  intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H10 H9)).
-  apply tech9; [ assumption | apply le_max_l ].
-  apply Rge_trans with (Un n - x0).
-  unfold Rminus in |- *; apply Rle_ge; do 2 rewrite <- (Rplus_comm (- x0));
-    apply Rplus_le_compat_l.
-  apply tech9; [ assumption | apply le_max_l ].
-  left; assumption.
-  unfold ge in |- *; apply le_max_r.
-  apply Rplus_lt_reg_r with x0.
-  rewrite Rplus_0_r; unfold Rminus in |- *; rewrite (Rplus_comm x0);
-    rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r;
-      apply H4; apply le_n.
-  intros; apply Rlt_le_trans with (Un n).
-  case (Rlt_le_dec x0 (Un n)); intro.
-  assumption.
-  elim n0; assumption.
-  apply tech9; assumption.
-  unfold bound in |- *; exists x; unfold is_lub in H0; elim H0; intros;
-    assumption.
-Qed.
-
 Lemma tech13 :
   forall (An:nat -> R) (k:R),
     0 <= k < 1 ->