proposition: Lemma pow_lt_mono_r : forall a b c, 1<a -> 0<=c -> b<c -> a^b < a^c.
proof: Proof. intros a b c Ha Hc H. destruct (lt_ge_cases b 0) as [Hb|Hb]. - rewrite pow_neg_r by trivial. apply pow_pos_nonneg; order'. - assert (H' : b<=c) by order. destruct (le_exists_sub _ _ H') as (d & EQ & Hd). rewrite EQ, pow_add_r; trivial. rewrite <- (mul_1_l (a^b)) at 1. apply mul_lt_mono_pos_r. + apply pow_pos_nonneg; order'. + apply pow_gt_1; trivial. apply lt_eq_cases in Hd; destruct Hd as [LT|EQ']; trivial. rewrite <- EQ' in *. rewrite add_0_l in EQ. order. Qed.
imports: NZAxioms NZMulOrder