proposition: Lemma negb_row_free m n (M : 'M[F]_(m, n)) : ~~ row_free M = [exists i, (row i M <= row' i M)%MS].
proof: Proof. exact/row_freePn/existsP. 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)