proposition: Lemma pow_lt_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 LT. - now apply pow_lt_mono_r. - destruct (le_gt_cases c b) as [LE|GT]; trivial. assert (a^c <= a^b) by (apply pow_le_mono_r; order'). order. Qed.
imports: NZAxioms NZMulOrder