proposition: Lemma simmxLR {P A B} : P \in unitmx -> reflect (A = conjmx (invmx P) B) (A ~_P B).
proof: Proof. by move=> Pu; rewrite conjVmx//; apply: (iffP (simmxRL Pu)) => ->; rewrite !mulmxA ?(mulmxK, mulmxKV, mulVmx, mulmxV, mul1mx, mulmx1). 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)