proposition: Fact binomial_gt n : forall p, n < p -> binomial n p = 0.
proof: Proof. induction n as [ | n IHn ]; intros [|] ?; simpl; auto; try lia. do 2 (rewrite IHn; try lia). Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)