derive_sqrt

Author: yosakaon

theories/realfun.v

@@ -1878,7 +1878,16 @@ rewrite -[x]sqrtK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)).
 - rewrite !sqrtK//; split; first exact: exprn_derivable.
   by rewrite exp_derive expr1 scaler1.
 - by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
-Unshelve. all: by end_near. Qed.
+  Unshelve. all: by end_near. Qed.
+
+Lemma derive_sqrt {K : realType} (r : K) : 0 < r ->
+   (Num.sqrt^`())%classic r = (2 * Num.sqrt r)^-1 :> K.
+Proof.
+move=> r0.
+rewrite derive1E.
+apply: derive_val.
+exact: is_derive1_sqrt.
+Qed.
 
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.