proposition: Lemma RInt_f : is_RInt f ( / exp 1) 1 1.
proof: Proof. have Haux1: (0 < /exp 1). apply Rinv_0_lt_compat. apply exp_pos. evar_last. apply: is_RInt_derive. move => x Hx. apply If. apply Rlt_le_trans with (2 := proj1 Hx). apply Rmin_case. by apply Haux1. by apply Rlt_0_1. move => x Hx. apply continuity_pt_filterlim. apply derivable_continuous_pt. exists (((2 - 2) - 2 * ln x) / x ^ 2) ; apply is_derive_Reals, Dfab. apply Rlt_le_trans with (2 := proj1 Hx). apply Rmin_case. by apply Haux1. by apply Rlt_0_1. rewrite /minus /= /plus /opp /= -[eq]/(@eq R). rewrite ln_Rinv. rewrite ln_exp. rewrite ln_1. ring. by apply exp_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)