proposition: Lemma row_freePn m n (M : 'M[F]_(m, n)) : reflect (exists i, (row i M <= row' i M)%MS) (~~ row_free M).
proof: Proof. rewrite -kermx_eq0; apply: (iffP (rowV0Pn _)) => [|[i0 /submxP[D rM]]]. move=> [v /sub_kermxP vM_eq0 /rV0Pn[i0 vi0_neq0]]; exists i0. have := vM_eq0; rewrite mulmx_sum_row (bigD1_ord i0)//=. move=> /(canRL (addrK _))/(canRL (scalerK _))->//. rewrite sub0r scalerN -scaleNr scalemx_sub// summx_sub// => l _. by rewrite scalemx_sub// -row_rowsub row_sub. exists (\row_j oapp (D 0) (- 1) (unlift i0 j)); last first. by apply/rV0Pn; exists i0; rewrite !mxE unlift_none/= oppr_eq0 oner_eq0. apply/sub_kermxP; rewrite mulmx_sum_row (bigD1_ord i0)//= !mxE. rewrite unlift_none scaleN1r rM mulmx_sum_row addrC -sumrB big1 // => l _. by rewrite !mxE liftK row_rowsub subrr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)