diff options
Diffstat (limited to 'theories/Reals/Binomial.v')
| -rw-r--r-- | theories/Reals/Binomial.v | 3 |
1 files changed, 1 insertions, 2 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]. |