proposition: Fact power_sinc k p : 2 <= p -> power k p < power (S k) p.
proof: Proof. intros Hp; rewrite power_S. rewrite <- (Nat.mul_1_l (power k p)) at 1. apply Nat.mul_lt_mono_pos_r; try lia. apply power_ge_1; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)