Merge pull request math-comp#986 from proux01/ler_sqrt

Generalize ler_sqrt

CHANGELOG_UNRELEASED.md

@@ -27,6 +27,10 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
   + generalized lemmas `big_set0` and `big_set` from semigroups
     to arbitrary binary operators
 
+- in `ssrnum.v`
+  + generalize `ler_sqrt`
+  + generalize `ler_psqrt` to use `nneg` instead of `pos`
+
 ### Renamed
 
 ### Removed

mathcomp/algebra/ssrnum.v

@@ -4158,23 +4158,24 @@ rewrite -(@ler_pXn2r R 2) ?nnegrE ?sqrtr_ge0 //.
 by rewrite !sqr_sqrtr // (le_trans pa).
 Qed.
 
-Lemma ler_psqrt : {in @pos R &, {mono sqrt : a b / a <= b}}.
+Lemma ler_psqrt : {in @nneg R &, {mono sqrt : a b / a <= b}}.
 Proof.
 apply: le_mono_in => x y x_gt0 y_gt0.
 rewrite !lt_neqAle => /andP[neq_xy le_xy].
-by rewrite ler_wsqrtr // eqr_sqrt ?ltW // neq_xy.
+by rewrite ler_wsqrtr // eqr_sqrt // neq_xy.
 Qed.
 
-Lemma ler_sqrt a b : 0 < b -> (sqrt a <= sqrt b) = (a <= b).
+Lemma ler_sqrt a b : 0 <= b -> (sqrt a <= sqrt b) = (a <= b).
 Proof.
-move=> b_gt0; have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt.
-by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
+move=> b_ge0; have [a_le0|a_gt0] := ler0P a; last first.
+  by rewrite ler_psqrt // nnegrE ltW.
+by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0).
 Qed.
 
 Lemma ltr_sqrt a b : 0 < b -> (sqrt a < sqrt b) = (a < b).
 Proof.
 move=> b_gt0; have [a_le0|a_gt0] := ler0P a; last first.
-  by rewrite (leW_mono_in ler_psqrt).
+  by rewrite (leW_mono_in ler_psqrt)//; apply: ltW.
 by rewrite ler0_sqrtr // sqrtr_gt0 b_gt0 (le_lt_trans a_le0).
 Qed.