proposition: Lemma pow_le_mono_r : forall a b c, 0<a -> b<=c -> a^b <= a^c.
proof: Proof. intros a b c Ha H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite (pow_neg_r _ _ Hb). apply pow_nonneg; order. - apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. + apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H]. apply lt_le_incl, pow_lt_mono_r; order. + nzsimpl; order. Qed.
imports: NZAxioms NZMulOrder