proposition: Fact binomial_n1 n : 1 <= n -> binomial n 1 = n.
proof: Proof. destruct n as [ | n ]; try lia; intros _. induction n as [ | n IHn ]; auto. rewrite binomial_SS, IHn, binomial_n0; lia. Qed.
imports: Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd)