proposition: Lemma small_nexp_resp_lt : forall (x : R) m n, [0] [<] x -> x [<] [1] -> m < n -> x[^]n [<] x[^]m.
proof: Proof. intros. cut (forall k : nat, 0 < k -> x[^]k [<] [1]). intro H2. replace n with (m + (n - m)). astepl (x[^]m[*]x[^] (n - m)). astepr (x[^]m[*][1]). apply mult_resp_less_lft. apply H2. lia. apply nexp_resp_pos. assumption. auto with arith. simple induction k. intro H2. exfalso. inversion H2. intros. elim n0. astepl x. assumption. intros. astepl (x[*]x[^]S n1). astepr ([1][*] ([1]:R)). apply mult_resp_less_both. apply less_leEq. assumption. assumption. apply less_leEq. apply nexp_resp_pos. assumption. assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)