proposition: Lemma binomial_fact : forall m n : nat, binomial (n + m) n * (factorial n * factorial m) = factorial (n + m).
proof: Proof. intros m; elim m; clear m. intros n; rewrite Nat.add_comm; simpl in |- *; rewrite binomial_def3; ring. intros m H' n; elim n; clear n. simpl in |- *; ring. intros n H'0. replace (S n + S m) with (S (n + S m)); [ idtac | auto ]. rewrite binomial_def4. apply trans_equal with (y := S m * factorial (S n + m) + S n * factorial (n + S m)). rewrite <- H'0; rewrite <- H'. replace (S n + m) with (n + S m); simpl in |- *; auto; ring. replace (n + S m) with (S n + m); simpl in |- *; auto; ring. Qed.
imports: Coq(Arith ArithRing Wf_nat)