proposition: Lemma mx_rsim_trans n1 n2 n3 (rG1 : reprG n1) (rG2 : reprG n2) (rG3 : reprG n3) : mx_rsim rG1 rG2 -> mx_rsim rG2 rG3 -> mx_rsim rG1 rG3.
proof: Proof. case=> [B1 defn1 freeB1 homB1] [B2 defn2 freeB2 homB2]. exists (B1 *m B2); rewrite /row_free ?mxrankMfree 1?defn1 // => x Gx. by rewrite mulmxA homB1 // -!mulmxA homB2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)