From 00d150f97842d47300a33e84c62de69e7f2169c3 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 31 Jan 2025 19:19:26 +0900
Subject: [PATCH 1/2] minor generalization

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
---
 CHANGELOG_UNRELEASED.md |  3 +++
 reals_stdlib/Rstruct.v  | 12 +++++++++++-
 2 files changed, 14 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 7ef2d342fe..9df4ba36fa 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -84,6 +84,9 @@
 - in `normedtype.v`:
   + lemmas `not_near_at_rightP`, `not_near_at_leftP`
 
+- in `Rstruct.v`:
+  + lemma `RsqrtE`
+
 ### Deprecated
 
 ### Removed
diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v
index 760cd14e50..df1acfd7f5 100644
--- a/reals_stdlib/Rstruct.v
+++ b/reals_stdlib/Rstruct.v
@@ -477,13 +477,23 @@ Proof. elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed.
 Lemma IZRposE (p : positive) : IZR (Z.pos p) = INR (nat_of_pos p).
 Proof. by rewrite -Pos_to_natE INR_IPR. Qed.
 
-Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
+Let ge0_RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.
 Proof.
 move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
 rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; last exact/RleP.
 by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP.
 Qed.
 
+Lemma RsqrtE x : sqrt x = Num.sqrt x.
+Proof.
+set Rx := Rbasic_fun.Rcase_abs x.
+have RxE : Rx = Rbasic_fun.Rcase_abs x by [].
+rewrite /R_sqrt.sqrt -RxE.
+move: RxE; case: Rbasic_fun.Rcase_abs => x0 RxE.
+  by rewrite RxE ler0_sqrtr//; exact/ltW/RltP.
+by rewrite /Rx -/(R_sqrt.sqrt _) ge0_RsqrtE //; exact/RleP/Rge_le.
+Qed.
+
 Lemma RpowE x n : pow x n = x ^+ n.
 Proof. by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.
 

From a61cddcb330fd7ecc01448ffcb0b24a2332532dc Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 31 Jan 2025 23:10:35 +0900
Subject: [PATCH 2/2] fix

---
 analysis_stdlib/showcase/uniform_bigO.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/analysis_stdlib/showcase/uniform_bigO.v b/analysis_stdlib/showcase/uniform_bigO.v
index 9ec3cd2645..49a724f32f 100644
--- a/analysis_stdlib/showcase/uniform_bigO.v
+++ b/analysis_stdlib/showcase/uniform_bigO.v
@@ -43,8 +43,7 @@ Definition OuPex (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
 Lemma ler_norm2 (x : normedR2) :
   `|x| <= sqrt (Rsqr (fst x) + Rsqr (snd x)) <= Num.sqrt 2 * `|x|.
 Proof.
-rewrite RsqrtE; last by rewrite addr_ge0 //; apply/RleP/Rle_0_sqr.
-rewrite !Rsqr_pow2 !RpowE; apply/andP; split.
+rewrite RsqrtE !Rsqr_pow2 !RpowE; apply/andP; split.
   by rewrite ge_max; apply/andP; split;
     rewrite -[`|_|]sqrtr_sqr ler_wsqrtr // (lerDl, lerDr) sqr_ge0.
 wlog lex12 : x / (`|x.1| <= `|x.2|).
@@ -79,7 +78,7 @@ Qed.
 
 Definition OuO (f : A -> R * R -> R^o) (g : R * R -> R^o) :=
   (fun x => f x.1 x.2) =O_ (filter_prod [set setT]%classic
-  (within P (nbhs (0%R:R^o,0%R:R^o))(*[filter of 0 : R^o * R^o]*))) (fun x => g x.2).
+  (within P (nbhs (0%R:R^o, 0%R:R^o))(*[filter of 0 : R^o * R^o]*))) (fun x => g x.2).
 
 Lemma OuP_to_O f g : OuP f g -> OuO f g.
 Proof.