proposition: Lemma pascal : forall n i:nat, (i < n)%nat -> C n i + C n (S i) = C (S n) (S i).
proof: Proof. intros. rewrite pascal_step3; [ idtac | assumption ]. replace (C n i + INR (n - i) / INR (S i) * C n i) with (C n i * (1 + INR (n - i) / INR (S i))) by ring. replace (1 + INR (n - i) / INR (S i)) with (INR (S n) / INR (S i)). - rewrite pascal_step1. + rewrite Rmult_comm; replace (S i) with (S n - (n - i))%nat. * rewrite <- pascal_step2. -- apply pascal_step1. apply Nat.le_trans with n. ++ apply le_minusni_n. apply Nat.lt_le_incl; assumption. ++ apply Nat.le_succ_diag_r. -- apply le_minusni_n. apply Nat.lt_le_incl; assumption. * rewrite Nat.sub_succ_l. -- cut ((n - (n - i))%nat = i). ++ intro; rewrite H0; reflexivity. ++ apply Nat.add_sub_eq_l, Nat.sub_add. apply Nat.lt_le_incl; assumption. -- apply le_minusni_n; apply Nat.lt_le_incl; assumption. + apply Nat.lt_le_incl; assumption. - unfold Rdiv. repeat rewrite S_INR. rewrite minus_INR. + cut (INR i + 1 <> 0). * intro. apply Rmult_eq_reg_l with (INR i + 1); [ idtac | assumption ]. rewrite Rmult_plus_distr_l. rewrite Rmult_1_r. do 2 rewrite (Rmult_comm (INR i + 1)). repeat rewrite Rmult_assoc. rewrite Rinv_l; [ idtac | assumption ]. ring. * rewrite <- S_INR. apply not_O_INR; discriminate. + apply Nat.lt_le_incl; assumption. Qed.
imports: Rbase Rfunctions PartSum