proposition: Lemma pow_le_mono_l : forall a b c, 0<=a<=b -> a^c <= b^c.
proof: Proof. intros a b c (Ha,H). destruct (lt_trichotomy c 0) as [Hc|[Hc|Hc]]. - rewrite !(pow_neg_r _ _ Hc); now nzsimpl. - rewrite Hc; now nzsimpl. - apply lt_eq_cases in H. destruct H as [H|H]; [|now rewrite <- H]. apply lt_le_incl, pow_lt_mono_l; now try split. Qed.
imports: NZAxioms NZMulOrder