proposition: Lemma pascal_step3 : forall n i:nat, (i < n)%nat -> C n (S i) = INR (n - i) / INR (S i) * C n i.
proof: Proof. intros; unfold C. cut (forall n:nat, fact (S n) = (S n * fact n)%nat). - intro. cut ((n - i)%nat = S (n - S i)). + intro. pattern (n - i)%nat at 2; rewrite H1. repeat rewrite H0; unfold Rdiv; repeat rewrite mult_INR; repeat rewrite Rinv_mult. rewrite <- H1; rewrite (Rmult_comm (/ INR (n - i))); repeat rewrite Rmult_assoc; rewrite (Rmult_comm (INR (n - i))); repeat rewrite Rmult_assoc; rewrite Rinv_l. * ring. * apply not_O_INR; apply minus_neq_O; assumption. + rewrite <- Nat.sub_succ_l. * simpl; reflexivity. * apply -> Nat.le_succ_l; assumption. - intro; reflexivity. Qed.
imports: Rbase Rfunctions PartSum