diff options
Diffstat (limited to 'mathcomp/real_closed')
| -rw-r--r-- | mathcomp/real_closed/polyorder.v | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/mathcomp/real_closed/polyorder.v b/mathcomp/real_closed/polyorder.v index f18ec89..2da4dc9 100644 --- a/mathcomp/real_closed/polyorder.v +++ b/mathcomp/real_closed/polyorder.v @@ -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. |