From d762ebb5a8c5191d49a75aa89ec34966de00eb9b Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 25 Aug 2016 17:44:06 +0200
Subject: better ltngtP

---
 mathcomp/real_closed/polyorder.v | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'mathcomp/real_closed')

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.
-- 
cgit v1.2.3