proposition: Lemma nexp_resp_le : forall c : R, [1] [<=] c -> forall m n, m <= n -> c[^]m [<=] c[^]n.
proof: Proof. intros. cut ([0] [<] c); intros. 2: apply less_leEq_trans with ([1]:R); [ apply pos_one | assumption ]. cut (c [#] [0]); intros. 2: apply Greater_imp_ap; assumption. cut (forall n : nat, c[^]n [#] [0]); intros H3. 2: apply nexp_resp_ap_zero; assumption. cut (forall n : nat, ([1][/] _[//]H3 n) [#] [0]); intros H4. 2: apply div_resp_ap_zero_rev; apply one_ap_zero. rstepl ([1][/] _[//]H4 m). rstepr ([1][/] _[//]H4 n). apply recip_resp_leEq. apply recip_resp_pos; apply nexp_resp_pos; assumption. eapply leEq_wdl. 2: apply nexp_distr_recip with (x_ := X0). eapply leEq_wdr. 2: apply nexp_distr_recip with (x_ := X0). apply nexp_resp_le'. apply less_leEq. apply recip_resp_pos; assumption. apply shift_div_leEq. assumption. astepr c; assumption. assumption. Qed.
imports: Coq.Arith.Arith CoRN.algebra.COrdCauchy Coq(Lia)