diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /theories/Reals/Rtrigo_def.v | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rtrigo_def.v')
-rw-r--r-- | theories/Reals/Rtrigo_def.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 7f62f538b..9588e4438 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -63,7 +63,7 @@ Proof. Defined. (* Value of [exp 0] *) -Lemma exp_0 : exp 0 = 1. +Lemma exp_0 : exp 0 = 1. Proof. cut (exp_in 0 (exp 0)). cut (exp_in 0 1). @@ -96,7 +96,7 @@ Qed. Definition cos_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n)). Lemma simpl_cos_n : - forall n:nat, cos_n (S n) / cos_n n = - / INR (2 * S n * (2 * n + 1)). + forall n:nat, cos_n (S n) / cos_n n = - / INR (2 * S n * (2 * n + 1)). Proof. intro; unfold cos_n in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add; unfold Rdiv in |- *; rewrite Rinv_mult_distr. @@ -176,7 +176,7 @@ Proof. assert (H0 := archimed_cor1 eps H). elim H0; intros; exists x. intros; rewrite simpl_cos_n; unfold R_dist in |- *; unfold Rminus in |- *; - rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; + rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; rewrite Rabs_Ropp; rewrite Rabs_right. rewrite mult_INR; rewrite Rinv_mult_distr. cut (/ INR (2 * S n) < 1). @@ -250,7 +250,7 @@ Definition cos (x:R) : R := let (a,_) := exist_cos (Rsqr x) in a. Definition sin_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n + 1)). Lemma simpl_sin_n : - forall n:nat, sin_n (S n) / sin_n n = - / INR ((2 * S n + 1) * (2 * S n)). + forall n:nat, sin_n (S n) / sin_n n = - / INR ((2 * S n + 1) * (2 * S n)). Proof. intro; unfold sin_n in |- *; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add; unfold Rdiv in |- *; rewrite Rinv_mult_distr. @@ -300,7 +300,7 @@ Proof. unfold Un_cv in |- *; intros; assert (H0 := archimed_cor1 eps H). elim H0; intros; exists x. intros; rewrite simpl_sin_n; unfold R_dist in |- *; unfold Rminus in |- *; - rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; + rewrite Ropp_0; rewrite Rplus_0_r; rewrite Rabs_Rabsolu; rewrite Rabs_Ropp; rewrite Rabs_right. rewrite mult_INR; rewrite Rinv_mult_distr. cut (/ INR (2 * S n) < 1). @@ -382,7 +382,7 @@ Qed. Lemma sin_antisym : forall x:R, sin (- x) = - sin x. Proof. intro; unfold sin in |- *; replace (Rsqr (- x)) with (Rsqr x); - [ idtac | apply Rsqr_neg ]. + [ idtac | apply Rsqr_neg ]. case (exist_sin (Rsqr x)); intros; ring. Qed. |