diff options
| author | Florent Hivert | 2016-11-17 01:33:36 +0100 |
|---|---|---|
| committer | Florent Hivert | 2016-11-17 01:33:36 +0100 |
| commit | 84cc11db01159b17a8dcf4d02dbe0549067d228f (patch) | |
| tree | 964ee247bbf305022235217e716578a37be0bf62 /mathcomp/real_closed/polyorder.v | |
| parent | 5daf14d44b9cd22c6b51b2b23b4eebe5f3aee79f (diff) | |
| parent | 23e57fb47874331c5feaace883513b7abecdff28 (diff) | |
Merge remote-tracking branch 'upstream/master' into fixdoc
Diffstat (limited to 'mathcomp/real_closed/polyorder.v')
| -rw-r--r-- | mathcomp/real_closed/polyorder.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/mathcomp/real_closed/polyorder.v b/mathcomp/real_closed/polyorder.v index f18ec89..f84abb6 100644 --- a/mathcomp/real_closed/polyorder.v +++ b/mathcomp/real_closed/polyorder.v @@ -1,4 +1,4 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) Require Import mathcomp.ssreflect.ssreflect. From mathcomp @@ -108,10 +108,7 @@ Qed. Lemma muP p x n : p != 0 -> (('X - x%:P)^+n %| p) && ~~(('X - x%:P)^+n.+1 %| p) = (n == \mu_x p). Proof. -move=> hp0; rewrite !root_le_mu//; case: (ltngtP n (\mu_x p))=> hn. -+ by rewrite ltnW//=. -+ by rewrite leqNgt hn. -+ by rewrite hn leqnn. +by move=> hp0; rewrite !root_le_mu//; case: (ltngtP n (\mu_x p)). Qed. Lemma mu_gt0 p x : p != 0 -> (0 < \mu_x p)%N = root p x. |