proposition: Lemma simmxW m n {P : 'M[F]_(m, n)} {A B} : row_free P -> P *m A = B *m P -> A ~_P B.
proof: Proof. by rewrite /(_ ~__ _)/= /conjmx => fP ->; rewrite mulmxKp. 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)