proposition: Lemma mxrank_leq_col_row : forall m n (M : 'M_(m, n)), mxrank M <= minn m n.
proof: Proof. case => [|m] [|n] //= M; rewrite ?(thinmx0,flatmx0,mxrank0,leq0n) //. rewrite /mxrank size_filter /smith_seq /=; case: smithP => /= P d Q _ _ _ _. by apply/(leq_trans (count_size _ _)); rewrite size_take; case: leqP. 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