proposition: Lemma binomial_le_power n i : binomial n i <= power n 2.
proof: Proof. destruct (le_lt_dec i n) as [ Hi | Hi ]. + change 2 with (1+1). rewrite Newton_nat_S. eapply Nat.le_trans. 2:{ apply sum_0n_le_one with (f := fun i => binomial n i * power i 1). apply le_n_S, Hi. } rewrite power_of_1; lia. + rewrite binomial_gt; auto; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)