proposition: Lemma pascal_step2 : forall n i:nat, (i <= n)%nat -> C (S n) i = INR (S n) / INR (S n - i) * C n i.
proof: Proof. intros; unfold C; replace (S n - i)%nat with (S (n - i)). - cut (forall n:nat, fact (S n) = (S n * fact n)%nat). + intro; repeat rewrite H0. unfold Rdiv; repeat rewrite mult_INR; repeat rewrite Rinv_mult. ring. + intro; reflexivity. - symmetry; apply Nat.sub_succ_l; assumption. Qed.
imports: Rbase Rfunctions PartSum