proposition: Lemma tensmx_mul (R : comRingType) m n p q r s (A : 'M[R]_(m,n)) (B : 'M[R]_(p,q)) (C : 'M[R]_(n, r)) (D : 'M[R]_(q, s)) : (A *t B) *m (C *t D) = (A *m C) *t (B *m D).
proof: Proof. apply/matrixP=> /= i j. case (mxtens_indexP i)=> [im ip] {i}; case (mxtens_indexP j)=> [jr js] {j}. rewrite !mxE !mxtens_indexK mulr_sum; apply: congr_big=> // k _. by rewrite !mxE !mxtens_indexK mulrCA !mulrA [C _ _ * A _ _]mulrC. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop ssralg matrix zmodp div)