proposition: Theorem binomial_comp : forall n m : nat, binomial (n + m) n = binomial (n + m) m.
proof: Proof. intros n m. apply simpl_mult_r with (n := factorial n); auto with arith. apply simpl_mult_r with (n := factorial m); auto with arith. repeat rewrite <- Nat.mul_assoc. pattern (n + m) at 2 in |- *; rewrite Nat.add_comm. pattern (factorial n * factorial m) at 2 in |- *; rewrite Nat.mul_comm. repeat rewrite binomial_fact; auto. rewrite (Nat.add_comm n); auto. Qed.
imports: Coq(Arith ArithRing Wf_nat)