is_derive1_sqrt lemma (#1679)

* add derive1_sqrt, sqrK

---------

Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>

Author: yosakaon

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,12 @@
 
 ### Added
 
+- in `unstable.v`:
+  + lemma `sqrK`
+
+- in `realfun.v`:
+  + instance `is_derive1_sqrt`
+
 ### Changed
 
 ### Renamed

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.

theories/realfun.v

@@ -1763,6 +1763,26 @@ 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=> 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.
+  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// 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.