proposition: Lemma small_nexp_resp_le : forall (x : R) m n, [0] [<=] x -> x [<=] [1] -> m <= n -> x[^]n [<=] x[^]m.
proof: Proof. intros. cut (forall k : nat, x[^]k [<=] [1]). intro. replace n with (m + (n - m)). astepl (x[^]m[*]x[^] (n - m)). astepr (x[^]m[*][1]). apply mult_resp_leEq_lft. apply H2. apply nexp_resp_nonneg. auto. auto with arith. simple induction k. apply leEq_reflexive. clear H1 n; intros. astepl (x[^]n[*]x); astepr (([1]:R)[*][1]). apply mult_resp_leEq_both; auto. apply nexp_resp_nonneg; auto. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)