proposition: Lemma invmx_out : {in [predC unitmx], invmx =1 id}.
proof: Proof. by move=> A; rewrite inE /= /invmx -if_neg => ->. 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)