proposition: Lemma is_perm_mxMl n (A B : 'M_n) : is_perm_mx A -> is_perm_mx (A *m B) = is_perm_mx B.
proof: Proof. case/is_perm_mxP=> s ->. apply/is_perm_mxP/is_perm_mxP=> [[t def_t] | [t ->]]; last first. by exists (s * t)%g; rewrite perm_mxM. exists (s^-1 * t)%g. by rewrite perm_mxM -def_t -!row_permE -row_permM mulVg row_perm1. 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)