proposition: Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c -> (b<=c <-> a^b <= a^c).
proof: Proof. intros a b c Ha Hc. split; intro LE. - apply pow_le_mono_r; order'. - destruct (le_gt_cases b c) as [LE'|GT]; trivial. assert (a^c < a^b) by (apply pow_lt_mono_r; order'). order. Qed.
imports: NZAxioms NZMulOrder