proposition: Theorem Xderive_pt_sqrt : forall f f' x, Xderive_pt f x f' -> Xderive_pt (fun x => Xsqrt (f x)) x (Xdiv f' (Xadd (Xsqrt (f x)) (Xsqrt (f x)))).
proof: Proof. intros f f' x Hf. xtotal. intro v. assert (Hx: (0 < r1)%R). { apply Rnot_le_lt; intro Hr1. apply Y. now rewrite sqrt_neg; [rewrite Rplus_0_r|]. } apply derivable_pt_lim_eq_locally with (comp sqrt (proj_fun v f)). apply locally_true_imp with (2 := derivable_imp_defined_gt _ _ _ _ R0 X Hx Hf). intros x (w, (Hw1, Hw2)). unfold comp, proj_fun. rewrite Hw2. destruct (is_negative_spec w). elim (Rlt_not_le _ _ Hw1). now left. apply refl_equal. unfold Rdiv. rewrite Rmult_comm. apply derivable_pt_lim_comp. apply Hf. unfold proj_fun. rewrite X. replace (sqrt r1 + sqrt r1)%R with (2 * sqrt r1)%R by ring. now apply derivable_pt_lim_sqrt. Qed.
imports: Coq(Reals) Flocq(Raux) Stdlib Xreal