proposition: Lemma great_nexp_resp_lt : forall (x : R) m n, [1] [<] x -> m < n -> x[^]m [<] x[^]n.
proof: Proof. intros. induction n as [| n Hrecn]; intros. exfalso. inversion H. cut (m <= n). intro. cut (x[^]n [<] x[^]S n). intro. elim (le_lt_eq_dec _ _ H0); intro y. apply less_transitive_unfolded with (x[^]n); auto. rewrite y. auto. astepl (x[^]n[*][1]). astepr (x[^]n[*]x). apply mult_resp_less_lft. auto. apply nexp_resp_pos. apply leEq_less_trans with ([1]:R). apply less_leEq. apply pos_one. auto. auto with arith. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)