proposition: Lemma is_derive_sqrt (f : R -> R) (x df : R) : is_derive f x df -> 0 < f x -> is_derive (fun x => sqrt (f x)) x (df / (2 * sqrt (f x))).
proof: Proof. intros Hf Hfx. evar_last. eapply is_derive_comp. by apply filterdiff_sqrt. by apply Hf. reflexivity. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis