proposition: Lemma is_perm_mxMr n (A B : 'M_n) : is_perm_mx B -> is_perm_mx (A *m B) = is_perm_mx A.
proof: Proof. case/is_perm_mxP=> s ->. rewrite -[s]invgK -col_permE -is_perm_mx_tr tr_col_perm row_permE. by rewrite is_perm_mxMl (perm_mx_is_perm, is_perm_mx_tr). 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)