proposition: Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b).
proof: Proof. intros a b Ha. split; intros Hb. - rewrite <- (pow_1_l b) by order. apply pow_lt_mono_l; try split; order'. - destruct (lt_trichotomy b 0) as [H|[H|H]]; trivial. + rewrite pow_neg_r in Hb; order'. + rewrite H, pow_0_r in Hb. order. Qed.
imports: NZAxioms NZMulOrder