diff options
| author | Reynald Affeldt | 2020-02-18 07:23:31 +0900 |
|---|---|---|
| committer | Reynald Affeldt | 2020-03-15 16:35:02 +0900 |
| commit | 56af8ab9d2890182ba67bb33a9561633b134b50f (patch) | |
| tree | 446405e857339c6228860be50207c6ed478f9db4 /mathcomp | |
| parent | d2443948206ddf78706add540c27341da4abc906 (diff) | |
just noticed a tentative use of a not yet existing lemma
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |