proposition: Fact power_ge_n k p : 2 <= p -> k <= power k p.
proof: Proof. intros Hp. induction k as [ | k IHk ]. + rewrite power_0; auto. + apply Nat.le_lt_trans with (2 := power_sinc _ Hp); auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)