From 0bc1691f356145b895012c6f842bfe2783a3e1a2 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 25 Aug 2020 04:40:09 +0200
Subject: Extracting a nonzero coefficient from a nonzero matrix

+ shortening some proofs
---
 mathcomp/algebra/mxalgebra.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

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

diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index 9a0034d..d94bc8e 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -2155,9 +2155,7 @@ rewrite -sum1_card (partition_big lsubmx nzC) => [|A]; last first.
   rewrite -[A]hsubmxK v0 -[n.+1]/(1 + n)%N -col_mx0.
   rewrite -[rsubmx _]vsubmxK -det_tr tr_row_mx !tr_col_mx !trmx0.
   by rewrite det_lblock [0]mx11_scalar det_scalar1 mxE mul0r.
-rewrite -sum_nat_const; apply: eq_bigr; rewrite /= -[n.+1]/(1 + n)%N => v nzv.
-case: (pickP (fun i => v i 0 != 0)) => [k nza | v0]; last first.
-  by case/eqP: nzv; apply/colP=> i; move/eqP: (v0 i); rewrite mxE.
+rewrite -sum_nat_const; apply: eq_bigr => /= v /cV0Pn[k nza].
 have xrkK: involutive (@xrow F _ _ 0 k).
   by move=> m A /=; rewrite /xrow -row_permM tperm2 row_perm1.
 rewrite (reindex_inj (inv_inj (xrkK (1 + n)%N))) /= -[n.+1]/(1 + n)%N.
-- 
cgit v1.2.3