summaryrefslogtreecommitdiff
path: root/theories/Reals/Cos_rel.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /theories/Reals/Cos_rel.v
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'theories/Reals/Cos_rel.v')
-rw-r--r--theories/Reals/Cos_rel.v23
1 files changed, 11 insertions, 12 deletions
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index ac8ffbeb..d410e14a 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Cos_rel.v 9178 2006-09-26 11:18:22Z barras $ i*)
+(*i $Id: Cos_rel.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -109,9 +109,10 @@ pose
C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
end).
ring_simplify.
+unfold Rminus.
replace
(* (- old ring compat *)
- (-1 *
+ (-
sum_f_R0
(fun k:nat =>
sum_f_R0
@@ -140,7 +141,6 @@ replace
(fun l:nat =>
C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
(sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
-(*rewrite Rplus_comm.*) (* compatibility old ring... *)
apply sum_decomposition.
apply sum_eq; intros.
unfold Wn in |- *.
@@ -154,8 +154,7 @@ apply Rmult_eq_compat_l.
replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
reflexivity.
omega.
-replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
-(*replace (* compatibility old ring... *)
+replace
(-
sum_f_R0
(fun k:nat =>
@@ -171,13 +170,13 @@ replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
(fun p:nat =>
(-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
- y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].*)
-apply Rmult_eq_compat_l.
+ y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].
rewrite scal_sum.
rewrite decomp_sum.
replace (sin_nnn 0%nat) with 0.
-rewrite Rmult_0_l; rewrite Rplus_0_l.
-replace (pred (S n)) with n; [ idtac | reflexivity ].
+rewrite Rplus_0_l.
+change (pred (S n)) with n.
+ (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *)
apply sum_eq; intros.
rewrite Rmult_comm.
unfold sin_nnn in |- *.
@@ -185,8 +184,8 @@ rewrite scal_sum.
rewrite scal_sum.
apply sum_eq; intros.
unfold Rdiv in |- *.
-repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm (/ INR (fact (2 * S i)))).
+(*repeat rewrite Rmult_assoc.*)
+(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *)
repeat rewrite <- Rmult_assoc.
rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
repeat rewrite <- Rmult_assoc.
@@ -216,7 +215,7 @@ apply INR_fact_neq_0.
apply INR_fact_neq_0.
reflexivity.
apply lt_O_Sn.
-ring.
+(* ring. *)
apply sum_eq; intros.
rewrite scal_sum.
apply sum_eq; intros.