From e9c284b97b76e214f417ccc33907853bc0b8aa8e Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 29 May 2019 15:37:31 +0300
Subject: incorporate new suggestions by @CohenCyril

---
 mathcomp/algebra/polydiv.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 2ac2c3e..b65742d 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -2238,7 +2238,7 @@ Proof.
 apply/eqP/idP=> [d0|]; last first.
   case/or3P; [by move/eqP->; rewrite div0p| by move/eqP->; rewrite divp0|].
   by move/divp_small.
-case: (eqVneq p 0) => [->//|pn0]; case: (eqVneq q 0) => [->//| qn0].
+case: eqVneq => // _; case: eqVneq => // qn0.
 move: (divp_eq p q); rewrite d0 mul0r add0r.
 move/(f_equal (fun x : {poly R} => size x)).
 by rewrite size_scale ?lc_expn_scalp_neq0 // => ->; rewrite ltn_modp qn0 !orbT.
-- 
cgit v1.2.3