diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-28 22:16:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-28 22:16:14 +0000 |
| commit | b730066fb4dfdeccd7b17538eda845d0048c68ca (patch) | |
| tree | 25e10bc3b9780ded7cbc6e7c27dc0c0993f966f0 /theories/Reals/Alembert.v | |
| parent | 98af1982684a02f9521d28594e0fa01ac3275083 (diff) | |
Nommage explicite de certains "intro" pour préserver la compatibilité
en préparation du passage à des inductifs à polymorphisme de sorte
("sigT R" va devenir de type le type de R, càd Set)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8670 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Alembert.v')
| -rw-r--r-- | theories/Reals/Alembert.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 3a67fff82..188d7ad3c 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -30,7 +30,7 @@ intros An H H0. cut (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). -intro; apply X. +intro X; apply X. apply completeness. unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2); [ intro | apply Rinv_0_lt_compat; prove_sup0 ]. @@ -107,7 +107,7 @@ red in |- *; intro; assert (H8 := H n); rewrite H7 in H8; replace (S x + 0)%nat with (S x); [ reflexivity | ring ]. symmetry in |- *; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. -intro; elim X; intros. +intro X; elim X; intros. apply existT with x; apply tech10; [ unfold Un_growing in |- *; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; @@ -418,7 +418,7 @@ intros An k Hyp H H0. cut (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) -> sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)). -intro; apply X. +intro X; apply X. apply completeness. assert (H1 := tech13 _ _ Hyp H0). elim H1; intros. @@ -517,7 +517,7 @@ rewrite H10 in H11; elim (Rlt_irrefl _ H11). replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ]. symmetry in |- *; apply tech2; assumption. exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity. -intro; elim X; intros. +intro X; elim X; intros. apply existT with x; apply tech10; [ unfold Un_growing in |- *; intro; rewrite tech5; pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r; @@ -559,11 +559,11 @@ rewrite <- Rabs_mult. rewrite Rabs_Rabsolu. unfold Rdiv in H3; apply H3; assumption. apply H0. -intro. +intro X. elim X; intros. apply existT with x. assumption. -intro. +intro X. elim X; intros. apply existT with x. assumption. @@ -581,7 +581,7 @@ intros. cut (sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l)). -intro. +intro X. elim X; intros. apply existT with x0. apply tech12; assumption. @@ -723,4 +723,4 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. red in |- *; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r). -Qed.
\ No newline at end of file +Qed. |