proposition: Lemma binomial_def2 : forall n m : nat, n < m -> binomial n m = 0.
proof: Proof. simple induction n; simpl in |- *; auto. intros m; case m; simpl in |- *; auto. intros H'; inversion H'; auto. intros n0 H' m; case m; simpl in |- *; auto. intros H'0; Contradict H'0; auto with arith. intros n1 H'0; repeat rewrite H'; auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat)