proposition: Corollary binomial_lt_power n i : binomial n i < power (S n) 2.
proof: Proof. apply Nat.le_lt_trans with (1 := binomial_le_power _ _), power_sinc; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)