From 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 Mon Sep 17 00:00:00 2001
From: Anton Trunov
Date: Wed, 29 May 2019 15:17:39 +0300
Subject: Replace eqVneq with eqPsym

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

(limited to 'mathcomp/algebra/poly.v')

diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index d898774..a3b9211 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -368,7 +368,7 @@ Lemma nil_poly p : nilp p = (p == 0).
 Proof. exact: size_poly_eq0. Qed.
 
 Lemma poly0Vpos p : {p = 0} + {size p > 0}.
-Proof. by rewrite lt0n size_poly_eq0; apply: eqVneq. Qed.
+Proof. by rewrite lt0n size_poly_eq0; case: eqVneq; [left | right]. Qed.
 
 Lemma polySpred p : p != 0 -> size p = (size p).-1.+1.
 Proof. by rewrite -size_poly_eq0 -lt0n => /prednK. Qed.
-- 
cgit v1.2.3