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/intdiv.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index edd2620..0a5bfde 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -969,7 +969,7 @@ without loss{IHa} /forallP/(_ (_, _))/= a_dvM: / [forall k, a %| M k.1 k.2]%Z.
     by exists i; rewrite mxE.
   exists R^T; last exists L^T; rewrite ?unitmx_tr //; exists d => //.
   rewrite -[M]trmxK dM !trmx_mul mulmxA; congr (_ *m _ *m _).
-  by apply/matrixP=> i1 j1; rewrite !mxE; case: eqPsym => // ->.
+  by apply/matrixP=> i1 j1; rewrite !mxE; case: eqVneq => // ->.
 without loss{nz_a a_dvM} a1: M a Da / a = 1.
   pose M1 := map_mx (divz^~ a) M; case/(_ M1 1)=> // [k|L uL [R uR [d dvD dM]]].
     by rewrite !mxE Da divzz nz_a.
-- 
cgit v1.2.3