proposition: Lemma is_perm_mxV (A : 'M_n) : is_perm_mx A^-1 = is_perm_mx A.
proof: Proof. apply/is_perm_mxP/is_perm_mxP=> [] [s defA]; exists s^-1%g. by rewrite -(invrK A) defA perm_mxV. by rewrite defA perm_mxV. 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)