Renommage dans Binomial.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3562 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 14 insertions, 15 deletions

diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v
index 8b5406ee78..2654a5f600 100644
--- a/theories/Reals/Binomial.v
+++ b/theories/Reals/Binomial.v
@@ -107,9 +107,8 @@ Apply lt_le_weak; Assumption.
 Qed.
 
 (*********************)
-(* Formule du binôme *)
 (*********************)
-Lemma binome : (x,y:R;n:nat) ``(pow (x+y) n)``==(sum_f_R0 [i:nat]``(C n i)*(pow x i)*(pow y (minus n i))`` n).
+Lemma binomial : (x,y:R;n:nat) ``(pow (x+y) n)``==(sum_f_R0 [i:nat]``(C n i)*(pow x i)*(pow y (minus n i))`` n).
 Intros; Induction n.
 Unfold C; Simpl; Unfold Rdiv; Repeat Rewrite Rmult_1r; Rewrite Rinv_R1; Ring.
 Pattern 1 (S n); Replace (S n) with (plus n (1)); [Idtac | Ring].
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index d1c167c568..15f68c1bb1 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -218,8 +218,8 @@ Apply Rlt_R0_R1.
 Unfold C; Apply RmaxLess1.
 Replace ``/(INR
       (mult (fact (mult (S (S O)) (S (plus n0 n))))
-      (fact (mult (S (S O)) (minus N n0)))))`` with ``(Binome.C (mult (S (S O)) (S (plus N n))) (mult (S (S O)) (S (plus n0 n))))/(INR (fact (mult (S (S O)) (S (plus N n)))))``.
-Apply Rle_trans with ``(Binome.C (mult (S (S O)) (S (plus N n))) (S (plus N n)))/(INR (fact (mult (S (S O)) (S (plus N n)))))``.
+      (fact (mult (S (S O)) (minus N n0)))))`` with ``(Binomial.C (mult (S (S O)) (S (plus N n))) (mult (S (S O)) (S (plus n0 n))))/(INR (fact (mult (S (S O)) (S (plus N n)))))``.
+Apply Rle_trans with ``(Binomial.C (mult (S (S O)) (S (plus N n))) (S (plus N n)))/(INR (fact (mult (S (S O)) (S (plus N n)))))``.
 Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) (S (plus N n)))))``).
 Apply Rle_monotony.
 Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
@@ -251,7 +251,7 @@ Assumption.
 Apply le_pred_n.
 Right.
 Unfold Rdiv; Rewrite Rmult_sym.
-Unfold Binome.C.
+Unfold Binomial.C.
 Unfold Rdiv; Repeat Rewrite <- Rmult_assoc.
 Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l.
@@ -265,7 +265,7 @@ Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite plus_INR; Ring.
 Apply le_n_2n.
 Apply INR_fact_neq_0.
 Unfold Rdiv; Rewrite Rmult_sym.
-Unfold Binome.C.
+Unfold Binomial.C.
 Unfold Rdiv; Repeat Rewrite <- Rmult_assoc.
 Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l.
@@ -598,8 +598,8 @@ Apply Rlt_R0_R1.
 Unfold C; Apply RmaxLess1.
 Replace ``/(INR
       (mult (fact (plus (mult (S (S O)) (S (plus n0 n))) (S O)))
-      (fact (plus (mult (S (S O)) (minus N n0)) (S O)))))`` with ``(Binome.C (mult (S (S O)) (S (S (plus N n)))) (plus (mult (S (S O)) (S (plus n0 n))) (S O)))/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``.
-Apply Rle_trans with ``(Binome.C (mult (S (S O)) (S (S (plus N n)))) (S (S (plus N n))))/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``.
+      (fact (plus (mult (S (S O)) (minus N n0)) (S O)))))`` with ``(Binomial.C (mult (S (S O)) (S (S (plus N n)))) (plus (mult (S (S O)) (S (plus n0 n))) (S O)))/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``.
+Apply Rle_trans with ``(Binomial.C (mult (S (S O)) (S (S (plus N n)))) (S (S (plus N n))))/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``.
 Unfold Rdiv; Do 2 Rewrite <- (Rmult_sym ``/(INR (fact (mult (S (S O)) (S (S (plus N n))))))``).
 Apply Rle_monotony.
 Left; Apply Rlt_Rinv; Apply INR_fact_lt_0.
@@ -635,7 +635,7 @@ Assumption.
 Apply le_pred_n.
 Right.
 Unfold Rdiv; Rewrite Rmult_sym.
-Unfold Binome.C.
+Unfold Binomial.C.
 Unfold Rdiv; Repeat Rewrite <- Rmult_assoc.
 Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l.
@@ -649,7 +649,7 @@ Rewrite mult_INR; Repeat Rewrite S_INR; Rewrite plus_INR; Ring.
 Apply le_n_2n.
 Apply INR_fact_neq_0.
 Unfold Rdiv; Rewrite Rmult_sym.
-Unfold Binome.C.
+Unfold Binomial.C.
 Unfold Rdiv; Repeat Rewrite <- Rmult_assoc.
 Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1l.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 46f6b1abbd..f1675e8d51 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -99,7 +99,7 @@ Unfold Rdiv; Rewrite Rmult_1r; Rewrite Rinv_R1; Ring.
 Unfold sin_nnn.
 Rewrite <- Rmult_Rplus_distr.
 Apply Rmult_mult_r.
-Rewrite binome.
+Rewrite binomial.
 Pose Wn := [i0:nat]``(C (mult (S (S O)) (S i)) i0)*(pow x i0)*
          (pow y (minus (mult (S (S O)) (S i)) i0))``.
 Replace (sum_f_R0
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index e9789e2615..936f943d35 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -33,7 +33,7 @@ Lemma exp_form : (x,y:R;n:nat) (lt O n) -> ``(E1 x n)*(E1 y n)-(Reste_E x y n)==
 Intros; Unfold E1.
 Rewrite cauchy_finite.
 Unfold Reste_E; Unfold Rminus; Rewrite Rplus_assoc; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Apply sum_eq; Intros.
-Rewrite binome.
+Rewrite binomial.
 Rewrite scal_sum; Apply sum_eq; Intros.
 Unfold C; Unfold Rdiv; Repeat Rewrite Rmult_assoc; Rewrite (Rmult_sym (INR (fact i))); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym.
 Rewrite Rmult_1r; Rewrite Rinv_Rmult.
@@ -886,4 +886,4 @@ Apply Rle_sym1; Left; Apply exp_pos.
 Rewrite Rminus_distr.
 Rewrite Rmult_1r; Unfold Rdiv; Rewrite <- Rmult_assoc; Rewrite Rminus_distr.
 Rewrite Rmult_1r; Rewrite exp_plus; Reflexivity.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 5a74e40258..1983099111 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -13,7 +13,7 @@ Require Rbase.
 Require Rfunctions.
 Require Rseries.
 Require PartSum.
-Require Binome.
+Require Binomial.
 
 (* TT Ak; 1<=k<=N *)
 Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of
diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v
index 407f1fa7c7..bd80fb9bc0 100644
--- a/theories/Reals/SeqSeries.v
+++ b/theories/Reals/SeqSeries.v
@@ -15,7 +15,7 @@ Require Export SeqProp.
 Require Export Rcomplet.
 Require Export PartSum.
 Require Export AltSeries.
-Require Export Binome.
+Require Export Binomial.
 Require Export Rsigma.
 Require Export Rprod.
 Require Export Cauchy_prod.