diff options
| author | Cyril Cohen | 2020-03-16 00:08:40 +0100 |
|---|---|---|
| committer | GitHub | 2020-03-16 00:08:40 +0100 |
| commit | 41a995ad5cb0c5c99e2629bae0699bdf13e73e22 (patch) | |
| tree | 446405e857339c6228860be50207c6ed478f9db4 /mathcomp | |
| parent | d2443948206ddf78706add540c27341da4abc906 (diff) | |
| parent | 56af8ab9d2890182ba67bb33a9561633b134b50f (diff) | |
Merge pull request #460 from affeldt-aist/spurious_lerr
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. |