proposition: Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d.
proof: Proof. intros a b c d ? ?. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. Qed.
imports: NZAxioms NZMulOrder