proposition: Lemma Dfab (a b : R) : forall x, 0 < x -> is_derive (fab a b) x (((b - a) - b * ln x) / x ^ 2).
proof: Proof. move => x Hx. evar_last. apply is_derive_div. apply @is_derive_plus. apply is_derive_const. apply is_derive_scal. now apply is_derive_Reals, derivable_pt_lim_ln. apply is_derive_id. by apply Rgt_not_eq. rewrite /Rdiv /plus /zero /one /=. field. by apply Rgt_not_eq. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)