proposition: Lemma pow_lt_mono_l : forall a b c, 0<c -> 0<=a<b -> a^c < b^c.
proof: Proof. intros a b c Hc. apply lt_ind with (4:=Hc). - solve_proper. - intros (Ha,H). nzsimpl; trivial; order. - clear c Hc. intros c Hc IH (Ha,H). nzsimpl; try order. apply mul_lt_mono_nonneg; trivial. + apply pow_nonneg; try order. + apply IH. now split. Qed.
imports: NZAxioms NZMulOrder