From 48cfb88b085606d90ad6c91e14b47faa69e350fb Mon Sep 17 00:00:00 2001
From: Lynda Bentoucha <lynda.bentoucha@etu.u-paris.fr>
Date: Mon, 7 Jul 2025 10:38:32 +0900
Subject: [PATCH 1/2] add derive1_sqrt

remove comments

point missing
---
 theories/realfun.v | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

diff --git a/theories/realfun.v b/theories/realfun.v
index 9051299acf..59214fb397 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1763,6 +1763,42 @@ Unshelve. all: by end_near. Qed.
 
 End is_derive_inverse.
 
+Global Instance is_derive1_sqrt {K : realType} (x : K) : 0 < x -> is_derive x 1 Num.sqrt (2 * Num.sqrt x)^-1.
+Proof.
+move=> x_gt0.
+have sqrtK : {in Num.pos, cancel (@Num.sqrt K) (fun x => x ^+ 2)}.
+  by move=> a a0; rewrite sqr_sqrtr// ltW.
+rewrite -[x]sqrtK//.
+apply: (@is_derive_inverse K (fun x => x ^+ 2)).
+- near=> z.
+  rewrite sqrtr_sqr gtr0_norm//.
+  have [xz|zx|->] := ltgtP z (Num.sqrt x); last first.
+  + by rewrite sqrtr_gt0.
+  + by rewrite (lt_trans _ zx)// sqrtr_gt0.
+  + move: xz.
+    near: z.
+    exists (Num.sqrt x / 2).
+      rewrite /=.
+      rewrite mulr_gt0 //.
+      by rewrite sqrtr_gt0 x_gt0.
+    move=> r/=.
+    move=> /[swap] rx.
+    rewrite gtr0_norm ?subr_gt0//ltrBlDl -ltrBlDr.
+    apply: le_lt_trans.
+    rewrite subr_ge0 ger_pMr.
+      rewrite invf_le1.
+        by rewrite ler1n.
+      by [].
+    by rewrite sqrtr_gt0.
+- near=> z.
+  exact: exprn_continuous.
+- rewrite !sqrtK//; split.
+    exact: exprn_derivable.
+  by rewrite exp_derive expr1 scaler1.
+- by rewrite mulf_neq0 ?pnatr_eq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
+Unshelve. all: by end_near. 
+Qed.
+
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.
 

From 3aab2e458c08d97d532100503e7a7a9ccee3c6f4 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 7 Jul 2025 15:07:46 +0900
Subject: [PATCH 2/2] sqrK

---
 CHANGELOG_UNRELEASED.md |  6 +++++
 classical/unstable.v    |  3 +++
 theories/realfun.v      | 50 ++++++++++++++---------------------------
 3 files changed, 26 insertions(+), 33 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5029a574ce..3bcc9f8ea2 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,12 @@
 
 ### Added
 
+- in `unstable.v`:
+  + lemma `sqrK`
+
+- in `realfun.v`:
+  + instance `is_derive1_sqrt`
+
 ### Changed
 
 ### Renamed
diff --git a/classical/unstable.v b/classical/unstable.v
index 50b3d4605d..159013ef15 100644
--- a/classical/unstable.v
+++ b/classical/unstable.v
@@ -483,3 +483,6 @@ Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R
 
 Export -(notations) Morphisms.
 End ProperNotations.
+
+Lemma sqrK {K : rcfType} : {in Num.pos, cancel (@Num.sqrt K) (fun x => x ^+ 2)}.
+Proof. by move=> r r0; rewrite sqr_sqrtr// ltW. Qed.
diff --git a/theories/realfun.v b/theories/realfun.v
index 59214fb397..6d8ef90218 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -1763,41 +1763,25 @@ Unshelve. all: by end_near. Qed.
 
 End is_derive_inverse.
 
-Global Instance is_derive1_sqrt {K : realType} (x : K) : 0 < x -> is_derive x 1 Num.sqrt (2 * Num.sqrt x)^-1.
-Proof.
-move=> x_gt0.
-have sqrtK : {in Num.pos, cancel (@Num.sqrt K) (fun x => x ^+ 2)}.
-  by move=> a a0; rewrite sqr_sqrtr// ltW.
-rewrite -[x]sqrtK//.
-apply: (@is_derive_inverse K (fun x => x ^+ 2)).
-- near=> z.
-  rewrite sqrtr_sqr gtr0_norm//.
-  have [xz|zx|->] := ltgtP z (Num.sqrt x); last first.
-  + by rewrite sqrtr_gt0.
-  + by rewrite (lt_trans _ zx)// sqrtr_gt0.
-  + move: xz.
-    near: z.
-    exists (Num.sqrt x / 2).
-      rewrite /=.
-      rewrite mulr_gt0 //.
-      by rewrite sqrtr_gt0 x_gt0.
-    move=> r/=.
-    move=> /[swap] rx.
-    rewrite gtr0_norm ?subr_gt0//ltrBlDl -ltrBlDr.
-    apply: le_lt_trans.
-    rewrite subr_ge0 ger_pMr.
-      rewrite invf_le1.
-        by rewrite ler1n.
-      by [].
+Global Instance is_derive1_sqrt {K : realType} (x : K) : 0 < x ->
+  is_derive x 1 Num.sqrt (2 * Num.sqrt x)^-1.
+Proof.
+move=> x0.
+rewrite -[x]sqrK//; apply: (@is_derive_inverse _ (fun x => x ^+ 2)).
+- near=> z; rewrite sqrtr_sqr gtr0_norm//.
+  have [xz|zx|->] := ltgtP z (Num.sqrt x); last 2 first.
+    by rewrite (lt_trans _ zx)// sqrtr_gt0.
     by rewrite sqrtr_gt0.
-- near=> z.
-  exact: exprn_continuous.
-- rewrite !sqrtK//; split.
-    exact: exprn_derivable.
+  move: xz; near: z; exists (Num.sqrt x / 2) => /=.
+    by rewrite divr_gt0 // sqrtr_gt0 x0.
+  move=> r/= => /[swap] rx; rewrite gtr0_norm ?subr_gt0//ltrBlDl -ltrBlDr.
+  apply: le_lt_trans.
+  by rewrite subr_ge0 ger_pMr ?sqrtr_gt0// invf_le1// ler1n.
+- by near=> z; exact: exprn_continuous.
+- rewrite !sqrK//; split; first exact: exprn_derivable.
   by rewrite exp_derive expr1 scaler1.
-- by rewrite mulf_neq0 ?pnatr_eq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
-Unshelve. all: by end_near. 
-Qed.
+- by rewrite mulf_neq0// gt_eqF// sqrtr_gt0 exprn_gt0// sqrtr_gt0.
+Unshelve. all: by end_near. Qed.
 
 #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) =>
   (eapply is_deriveV; first by []) : typeclass_instances.