proposition: Lemma pascal_step1 : forall n i:nat, (i <= n)%nat -> C n i = C n (n - i).
proof: Proof. intros; unfold C; replace (n - (n - i))%nat with i. - rewrite Rmult_comm. reflexivity. - symmetry; apply Nat.add_sub_eq_l, Nat.sub_add; assumption. Qed.
imports: Rbase Rfunctions PartSum