Adapt to math-comp/math-comp#986

proux01 · Nov 24, 2023 · ab938b2 · ab938b2
1 parent e3a557e
commit ab938b2
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
@@ -585,12 +585,13 @@ Arguments dfwith {I T} f i x.
 
 Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).
 
+(* MathComp 2.2 addition *)
 Lemma ler_sqrt {R : rcfType} (a b : R) :
   (0 <= b -> (Num.sqrt a <= Num.sqrt b) = (a <= b))%R.
 Proof.
 have [b_gt0 _|//|<- _] := ltgtP; last first.
   by rewrite sqrtr0 -sqrtr_eq0 le_eqVlt ltNge sqrtr_ge0 orbF.
-have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt.
+have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt// ?qualifE/= ?ltW.
 by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
 Qed.