proposition: Theorem binomial_lt : forall n m : nat, 0 < n -> 0 < binomial (n + m) n.
proof: Proof. intros n; elim n. intros m H; inversion H. intros n1; case n1. intros H m; elim m; simpl in |- *; auto with arith. intros n2 Rec m H1. change (0 < binomial (S n2 + m) (S (S n2)) + binomial (S n2 + m) (S n2)) in |- *; auto with arith. apply Nat.lt_le_trans with (0 + binomial (S n2 + m) (S n2)); auto with arith. apply (Rec m); auto with arith. Qed.
imports: Coq(Arith ArithRing Wf_nat)