proposition: Lemma lift0_mx_perm s : lift0_mx (perm_mx s) = perm_mx (lift0_perm s).
proof: Proof. apply/matrixP=> /= i j; rewrite !mxE split1 /=; case: unliftP => [i'|] -> /=. rewrite lift0_perm_lift !mxE split1 /=. by case: unliftP => [j'|] ->; rewrite ?(inj_eq (lift_inj _)) /= !mxE. rewrite lift0_perm0 !mxE split1 /=. by case: unliftP => [j'|] ->; rewrite /= mxE. 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)