proposition: Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> a^b < c^d.
proof: Proof. intros a b c d (Ha,Hac) (Hb,Hbd). apply le_succ_l in Ha; rewrite <- one_succ in Ha. apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha]. - transitivity (a^d). + apply pow_lt_mono_r; intuition order. + apply pow_lt_mono_l; try split; order'. - nzsimpl; try order. apply pow_gt_1; order. Qed.
imports: NZAxioms NZMulOrder