proposition: Fact power_smono_l p q x : 2 <= x -> p < q -> power p x < power q x.
proof: Proof. intros H1 H2. apply Nat.lt_le_trans with (1 := power_sinc _ H1). apply power_mono_l; lia. Qed.
imports: List Arith ZArith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list binomial)