proposition: Fact power_mono_r n p q : p <= q -> power n p <= power n q.
proof: Proof. intros H. induction n as [ | n IHn ]. + do 2 rewrite power_0; auto. + do 2 rewrite power_S; apply Nat.mul_le_mono; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)