From 037c72f8de1f8a168199ed75934ecb842dd02412 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 24 Nov 2023 16:40:19 +0100 Subject: [PATCH] Adapt to https://github.com/math-comp/math-comp/pull/986 --- classical/mathcomp_extra.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 3b1a5a188..a49e3bc4a 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1138,12 +1138,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.