proposition: Lemma section_eqmx U1 U2 V1 V2 modU1 modU2 modV1 modV2 (eqU : (U1 :=: U2)%MS) (eqV : (V1 :=: V2)%MS) : mx_rsim (@section_repr U1 V1 modU1 modV1) (@section_repr U2 V2 modU2 modV2).
proof: Proof. by apply: section_eqmx_add => //; apply: adds_eqmx. 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)