proposition: Fact power_mono_l p q x : 1 <= x -> p <= q -> power p x <= power q x.
proof: Proof. intros Hx. induction 1 as [ | q H IH ]; auto. apply Nat.le_trans with (1 := IH). rewrite power_S. rewrite <- (Nat.mul_1_l (power _ _)) at 1. apply Nat.mul_le_mono; auto. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)