proposition: Lemma nexp_resp_le' : forall c : R, [0] [<=] c -> c [<=] [1] -> forall m n, m <= n -> c[^]n [<=] c[^]m.
proof: Proof. intros. astepl ([0][+]c[^]n); apply shift_plus_leEq. set (N := n - m) in *. apply leEq_wdr with (c[^]m[-]c[^]m[*]c[^]N). rstepr (c[^]m[*] ([1][-]c[^]N)). astepl (([0]:R)[*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive. apply nexp_resp_nonneg; auto. apply shift_leEq_minus. astepl (c[^]N). apply nexp_resp_leEq_one; assumption. apply cg_minus_wd. algebra. eapply eq_transitive_unfolded. apply nexp_plus. replace n with (m + (n - m)). algebra. auto with arith. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)