proposition: Lemma simmxP {P A B} : P \in unitmx -> reflect (P *m A = B *m P) (A ~_P B).
proof: Proof. move=> p_unit; apply: (iffP idP); first exact/simmxPp/stablemx_unit. by apply: simmxW; rewrite row_free_unit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)