From fbeec199e65fe7e9fd96ddd74e31aa0461c22927 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 1 Sep 2020 15:44:13 +0200
Subject: Lemmas reindex_omap and bigD1_ord

+ eq_liftF and lift_eqF
+ proof simplificaions
---
 mathcomp/algebra/mxpoly.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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

diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index cbac070..f33e291 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -188,7 +188,7 @@ have: rj0T (Ss_ dj.+1) = 'X^dj *: rj0T (S_ j1) + 1 *: rj0T (Ss_ dj).
   rewrite Sylvester_mxE insubdK; last exact: leq_ltn_trans (ltjS).
   by have [->|] := eqP; rewrite (addr0, add0r).
 rewrite -det_tr => /determinant_multilinear->;
-  try by apply/matrixP=> i j; rewrite !mxE eq_sym (negPf (neq_lift _ _)).
+  try by apply/matrixP=> i j; rewrite !mxE lift_eqF.
 have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r.
   rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _].
     rewrite add0r; congr (\det _)%:P.
-- 
cgit v1.2.3