From 56af8ab9d2890182ba67bb33a9561633b134b50f Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Tue, 18 Feb 2020 07:23:31 +0900
Subject: just noticed a tentative use of a not yet existing lemma

---
 mathcomp/algebra/ssrnum.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index f9b4cb0..78286cc 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1342,7 +1342,7 @@ Lemma poly_ivt : real_closed_axiom R. Proof. by case: R => ? []. Qed.
 Fact sqrtr_subproof (x : R) :
   exists2 y, 0 <= y & (if 0 <= x then y ^+ 2 == x else y == 0) : bool.
 Proof.
-case x_ge0: (0 <= x); last by exists 0; rewrite ?lerr.
+case x_ge0: (0 <= x); last by exists 0.
 have le0x1: 0 <= x + 1 by rewrite -nnegrE rpredD ?rpred1.
 have [|y /andP[y_ge0 _]] := @poly_ivt ('X^2 - x%:P) _ _ le0x1.
   rewrite !hornerE -subr_ge0 add0r opprK x_ge0 -expr2 sqrrD mulr1.
-- 
cgit v1.2.3