proposition: Lemma trmx_mul_rev (R : semiRingType) m n p (A : 'M[R]_(m, n)) (B : 'M[R]_(n, p)) : (A *m B)^T = (B : 'M[R^c]_(n, p))^T *m (A : 'M[R^c]_(m, n))^T.
proof: Proof. by apply/matrixP=> k i /[!mxE]; apply: eq_bigr => j _ /[!mxE]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)