proposition: Lemma mxtrace_sub_fact_mod x : \tr (submod_repr x) + \tr (factmod_repr x) = \tr (rG x).
proof: Proof. rewrite -[submod_repr x]mulmxA mxtrace_mulC -val_submodE addrC. rewrite -[factmod_repr x]mulmxA mxtrace_mulC -val_factmodE addrC. by rewrite -mxtraceD add_sub_fact_mod. 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)