proposition: Lemma mxrank_leq_row m n (M : 'M_(m, n)) : mxrank M <= m.
proof: Proof. by move: (mxrank_leq_col_row M); rewrite leq_min; case/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent