proposition: Lemma If : forall x, 0 < x -> is_derive (fun y : R => 2 * ln y + (ln y) ^ 2) x (f x).
proof: Proof. move => y Hy. evar_last. apply @is_derive_plus. apply is_derive_Reals. apply derivable_pt_lim_scal. by apply derivable_pt_lim_ln. apply is_derive_pow. by apply is_derive_Reals, derivable_pt_lim_ln. rewrite /f /fab /plus /= ; field. by apply Rgt_not_eq. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)