proposition: Lemma diff_xlnx_sincreasing_0_Rinv_e2 : forall x y : R, 0 <= x <= exp (-2) -> 0 <= y <= exp (-2) -> x < y -> diff_xlnx x < diff_xlnx y.
proof: Proof. apply derive_sincreasing_interv. - move=> x /= [Hx1 Hx2]. apply derivable_pt_diff_xlnx. split => //. exact: (ltR_trans Hx2 ltRinve21). - move=> x /= Hx. rewrite /diff_xlnx. apply continuity_pt_minus ; last by apply continue_xlnx. apply (continuity_pt_comp (fun x => 1 - x) xlnx); last by apply continue_xlnx. apply continuity_pt_plus ; first by apply continuity_pt_const. apply continuity_pt_opp. apply derivable_continuous_pt. by apply derivable_pt_id. - by apply exp_pos. - move => t prt [Ht1 Ht2]. apply derive_diff_xlnx_pos => //. exact: (conj Ht1 (ltR_trans Ht2 ltRinve21)). Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) mathcomp(Rstruct) Reals Lra ssrR realType_ext Reals_ext Ranalysis_ext logb convex