diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-09 15:42:49 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-09 15:42:49 +0000 |
| commit | 15da5979d322c5da5f251dfd92da26407df5e45f (patch) | |
| tree | e523eaad6988c9731fc8868bb20f234ce7934120 /theories/Reals/Rtrigo_alt.v | |
| parent | d63861313993ed3d0a0108d659e0b08a215442c1 (diff) | |
retour en arriere concernant la recherche d'occurence modulo expansion des letins, ce qui conduisait a des comportement peu intuitifs. On priviligiera l'utilisation de la tactique Subst.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3110 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_alt.v')
| -rw-r--r-- | theories/Reals/Rtrigo_alt.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 4815028c0..5cdfd96ce 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -219,7 +219,7 @@ Apply pow_lt; Assumption. Apply Rlt_Rinv; Apply lt_INR_0; Apply neq_O_lt; Red; Intro; Assert H8 := (sym_eq ? ? ? H7); Elim (fact_neq_0 ? H8). Clear Un Vn; Apply INR_le; Simpl. Induction M_nat. -Assert H6 := (archimed (Rabsolu x)); Elim H6; Intros; Fold M in H6. +Assert H6 := (archimed (Rabsolu x)); Fold M in H6; Elim H6; Intros. Rewrite H4 in H7; Rewrite <- INR_IZR_INZ in H7. Simpl in H7; Elim (Rlt_antirefl ? (Rlt_trans ? ? ? H2 H7)). Replace R1 with (INR (S O)); [Apply le_INR | Reflexivity]; Apply le_n_S; Apply le_O_n. @@ -515,4 +515,4 @@ Left; Assumption. Rewrite <- (Ropp_Ropp ``PI/2``); Apply Rle_Ropp1; Unfold Rdiv; Unfold Rdiv in H0; Rewrite <- Ropp_mul1; Exact H0. Intros; Unfold cos_approx; Apply sum_eq; Intros; Unfold cos_term; Do 2 Rewrite pow_Rsqr; Rewrite Rsqr_neg; Unfold Rdiv; Reflexivity. Apply Rgt_RO_Ropp; Assumption. -Qed.
\ No newline at end of file +Qed. |