diff options
| author |  desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 13:11:19 +0000 |
|---|---|---|
| committer | desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 13:11:19 +0000 |
| commit | d5ab2a4d38a38db278a78e67d762c052b8e8e606 (patch) | |
| tree | b98ecec33e2d08f4ce78ed2ec04e6899972bbdb2 /theories/Reals/Rtrigo_alt.v | |
| parent | 314333e2ce7c06293ab6e5292b2927afb75b6a6f (diff) | |
Renommages dans PartSum
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3574 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 37a908037..99d6a736b 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -129,7 +129,7 @@ Unfold sin; Case (exist_sin (Rsqr a)). Intros; Cut x==x0. Intro; Rewrite H3; Unfold Rdiv. Symmetry; Apply Rinv_r_simpl_m; Assumption. -Unfold sin_in in p; Unfold sin_in in s; EApply unicite_sum. +Unfold sin_in in p; Unfold sin_in in s; EApply unicity_sum. Apply p. Apply s. Intros; Elim H2; Intros. @@ -251,7 +251,7 @@ Rewrite pow_Rsqr; Reflexivity. Simpl; Ring. Unfold cos_n; Unfold Rdiv; Simpl; Rewrite Rinv_R1; Rewrite Rmult_1r; Reflexivity. Apply lt_O_Sn. -Unfold cos; Case (exist_cos (Rsqr a0)); Intros; Unfold cos_in in p; Unfold cos_in in c; EApply unicite_sum. +Unfold cos; Case (exist_cos (Rsqr a0)); Intros; Unfold cos_in in p; Unfold cos_in in c; EApply unicity_sum. Apply p. Apply c. Intros; Elim H3; Intros; Replace ``(cos a0)-1`` with ``-(1-(cos a0))``; [Idtac | Ring]. |