diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b..990421a2f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `realfun.v`:
+  + lemma `derivable_sqrt`
+
 ### Changed
 
 ### Renamed
diff --git a/theories/realfun.v b/theories/realfun.v
index 961e22a35..97e929d60 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1943,9 +1943,12 @@ rewrite -[x]sqrtK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)).
 - by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
 Unshelve. all: by end_near. Qed.
 
+Lemma derivable_sqrt {K : realType} (x : K) : 0 < x -> derivable Num.sqrt x 1.
+Proof.  by move=> x0; exact/ex_derive/is_derive1_sqrt. Qed.
+
 Lemma derive_sqrt {K : realType} (r : K) : 0 < r ->
   'D_1 Num.sqrt r = (2 * Num.sqrt r)^-1.
-Proof. by move=> r0; apply: derive_val; exact: is_derive1_sqrt. Qed.
+Proof. by move=> r0; exact/derive_val/is_derive1_sqrt. Qed.
 
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.