proposition: Lemma mul_1tensmx (cR : comRingType) (m n p: nat) (e3n : (n + (n + n) = 3 * n)%N) (A B C : 'M[cR]_(m, n)) (M : 'M[cR]_(n, p)) : castmx (erefl _, e3n) (row_mx A (row_mx B C)) *m (1%:M *t M) = castmx (erefl _, esym (mul3n _)) (row_mx (A *m M) (row_mx (B *m M) (C *m M))).
proof: Proof. apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. rewrite tens_I3_mx mulmx_cast castmx_mul !castmx_comp /= !castmx_id /=. by rewrite !mul_row_block /= !mulmx0 !addr0 !add0r. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)