proposition: Lemma pow_gt_lin_r : forall a b, 1<a -> 0<=b -> b < a^b.
proof: Proof. intros a b Ha Hb. apply le_ind with (4:=Hb). - solve_proper. - nzsimpl. order'. - clear b Hb. intros b Hb IH. nzsimpl; trivial. rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha. transitivity (2*(S b)). + nzsimpl'. rewrite <- 2 succ_le_mono. rewrite <- (add_0_l b) at 1. apply add_le_mono; order. + apply mul_le_mono_nonneg; trivial. * order'. * now apply lt_le_incl, lt_succ_r. Qed.
imports: NZAxioms NZMulOrder