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