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