proposition: Lemma invmxK : involutive invmx.
proof: Proof. move=> A; case uA : (A \in unitmx); last by rewrite /invmx !uA. by apply: (can_inj (mulKVmx uA)); rewrite mulVmx // mulmxV ?unitmx_inv. 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)