diff options
| author | Cyril Cohen | 2016-08-25 17:44:06 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2016-10-24 13:11:31 +0200 |
| commit | d762ebb5a8c5191d49a75aa89ec34966de00eb9b (patch) | |
| tree | 6bc0abd5084ef9db1ff09ae5690bf75df4d63b73 /mathcomp/real_closed | |
| parent | fb7060ca71082911284ff6b388c3c45ef07c2723 (diff) | |
better ltngtP
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. |