proposition: Lemma is_derive_ln x : 0 < x -> is_derive ln x (/ x)%R.
proof: Proof. intros H. apply is_derive_Reals. now apply derivable_pt_lim_ln. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis