proposition: Lemma mxrank_eq0 m n (A : 'M_(m, n)) : (\rank A == 0) = (A == 0).
proof: Proof. apply/eqP/eqP=> [rA0 | ->{A}]; last exact: mxrank0. move: (col_base A) (row_base A) (mulmx_base A); rewrite rA0 => Ac Ar <-. by rewrite [Ac]thinmx0 mul0mx. 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)