proposition: Lemma binomial_lt n p : n < p -> binomial n p = 0.
proof: Proof. revert p. induction n; intros [ | p ] H. - lia. - reflexivity. - lia. - simpl. rewrite IHn. 2:lia. rewrite IHn; lia. Qed.
imports: Arith ZArith String List Psatz Factorial