proposition: Lemma filterdiff_sqrt (x : R) : 0 < x -> filterdiff sqrt (locally x) (fun y => scal y (/ (2 * sqrt x))).
proof: Proof. intros Hx. apply is_derive_Reals. by apply derivable_pt_lim_sqrt. Qed.
imports: Coq(Reals Lia ssreflect) Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries Lim_seq RInt_analysis