proposition: Lemma memmx0 n A : (A \in (0 : 'A_n)) -> A = 0.
proof: Proof. by rewrite submx0 mxvec_eq0; move/eqP. 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)