proposition: Lemma tens_I3_mx (cR : comRingType) m n (M : 'M[cR]_(m,n)) : 1%:M *t M = castmx (esym (mul3n _ ), esym (mul3n _ )) (block_mx M 0 0 (block_mx M 0 0 M : 'M_(m+m,n+n)%N)).
proof: Proof. rewrite [1%:M : 'M_(1+2)%N]scalar_mx_block. rewrite [1%:M : 'M_(1+1)%N]scalar_mx_block. rewrite !tens_block_mx. apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. rewrite castmx_comp !tens_scalar_mx !tens0mx !scale1r. rewrite (castmx_block (mul1n _) (mul1n _) (mul2n _) (mul2n _)). rewrite !castmx_comp /= !castmx_id. rewrite (castmx_block (mul1n _) (mul1n _) (mul1n _) (mul1n _)). by rewrite !castmx_comp /= !castmx_id !castmx_const /=. 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)