4 files changed, 10 insertions, 12 deletions
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.
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v
index ff9d43a..9d6e2be 100644
--- a/mathcomp/algebra/matrix.v
+++ b/mathcomp/algebra/matrix.v
@@ -1392,7 +1392,7 @@ Definition diag_mx n (d : 'rV[R]_n) :=
   \matrix[diag_mx_key]_(i, j) (d 0 i *+ (i == j)).
 
 Lemma tr_diag_mx n (d : 'rV_n) : (diag_mx d)^T = diag_mx d.
-Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqPsym => // ->. Qed.
+Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed.
 
 Lemma diag_mx_is_linear n : linear (@diag_mx n).
 Proof.
@@ -1744,7 +1744,7 @@ by rewrite eqn_leq andbC leqNgt lshift_subproof.
 Qed.
 
 Lemma tr_pid_mx m n r : (pid_mx r)^T = pid_mx r :> 'M_(n, m).
-Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqPsym => // ->. Qed.
+Proof. by apply/matrixP=> i j; rewrite !mxE; case: eqVneq => // ->. Qed.
 
 Lemma pid_mx_minv m n r : pid_mx (minn m r) = pid_mx r :> 'M_(m, n).
 Proof. by apply/matrixP=> i j; rewrite !mxE leq_min ltn_ord. Qed.
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.
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 6f9d837..2ac2c3e 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -2037,8 +2037,7 @@ Lemma egcdp_recP : forall k p q, q != 0 -> size q <= k -> size q <= size p ->
     [/\ size e.1 <= size q, size e.2 <= size p & gcdp p q %= e.1 * p + e.2 * q].
 Proof.
 elim=> [|k ihk] p q /= qn0; first by rewrite leqn0 size_poly_eq0 (negPf qn0).
-move=> sqSn qsp; case: (eqVneq q 0)=> q0; first by rewrite q0 eqxx in qn0.
-rewrite (negPf qn0).
+move=> sqSn qsp; rewrite (negPf qn0).
 have sp : size p > 0 by apply: leq_trans qsp; rewrite size_poly_gt0.
 case: (eqVneq (p %% q) 0) => [r0 | rn0] /=.
   rewrite r0 /egcdp_rec; case: k ihk sqSn => [|n] ihn sqSn /=.
@@ -2239,8 +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]; first by rewrite eqxx.
-case: (eqVneq q 0) => [-> | qn0]; first by rewrite eqxx orbT.
+case: (eqVneq p 0) => [->//|pn0]; case: (eqVneq q 0) => [->//| 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.
@@ -3039,8 +3037,8 @@ Proof.
 move=> eqr; rewrite /gdcop; move: (size p)=> n.
 elim: n p q r eqr {1 3}p (eqpxx p) => [|n ihn] p q r eqr s esp /=.
   move: eqr; case: (eqVneq q 0)=> [-> | nq0 eqr] /=.
-    by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx.
-  suff rn0 : r != 0 by rewrite (negPf nq0) (negPf rn0) eqpxx.
+    by rewrite eqp_sym eqp0 => ->; rewrite eqpxx.
+  suff rn0 : r != 0 by rewrite (negPf rn0) eqpxx.
   by apply: contraTneq eqr => ->; rewrite eqp0.
 rewrite (eqp_coprimepr _ eqr) (eqp_coprimepl _ esp); case: ifP=> _ //.
 by apply: ihn => //; apply: eqp_div => //; apply: eqp_gcd.
@@ -3051,8 +3049,8 @@ Proof.
 rewrite /rgdcop /gdcop; move: (size p)=> n.
 elim: n p q {1 3}p {1 3}q (eqpxx p) (eqpxx q) => [|n ihn] p q s t /= sp tq.
   move: tq; case: (eqVneq t 0)=> [-> | nt0 etq].
-    by rewrite eqp_sym eqp0; move->; rewrite eqxx eqpxx.
-  suff qn0 : q != 0 by rewrite (negPf nt0) (negPf qn0) eqpxx.
+    by rewrite eqp_sym eqp0 => ->; rewrite eqpxx.
+  suff qn0 : q != 0 by rewrite (negPf qn0) eqpxx.
   by apply: contraTneq etq => ->; rewrite eqp0.
 rewrite rcoprimep_coprimep (eqp_coprimepl t sp) (eqp_coprimepr p tq).
 case: ifP=> // _; apply: ihn => //; apply: eqp_trans (eqp_rdiv_div _ _) _.