proposition: Lemma flatmx0 n : all_equal_to (0 : 'M_(0, n)).
proof: Proof. by move=> A; apply/matrixP=> [] []. 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 countalg finalg zmodp)