diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-18 19:31:47 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-02-18 19:31:47 +0000 |
| commit | bffb49355300fc298b286b6ab33cc65c2eed716d (patch) | |
| tree | 392b1375a0f4c7e7b6c8222baa77ec2f361af957 /theories/Reals/Alembert.v | |
| parent | 737d1b8008783e0c558065ca0836412f0c9b0e0d (diff) | |
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
Diffstat (limited to 'theories/Reals/Alembert.v')
| -rw-r--r-- | theories/Reals/Alembert.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 6e2488f5d..ef75323e0 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -109,7 +109,7 @@ Proof. symmetry in |- *; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. intro X; elim X; intros. - exists x; apply tech10; + exists x; apply Un_cv_crit_lub; [ unfold Un_growing in |- *; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H @@ -524,7 +524,7 @@ Proof. symmetry in |- *; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. intro X; elim X; intros. - exists x; apply tech10; + exists x; apply Un_cv_crit_lub; [ unfold Un_growing in |- *; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; apply H |