proposition: Lemma tens_ctmat1_mx n (M : 'M_n) : ctmat1 *t M = castmx (esym (mul3n _ ), esym (mul3n _ )) (block_mx M (row_mx M M) (col_mx (-M) 0) (block_mx M M 0 M : 'M_(n+n)%N)).
proof: Proof. rewrite ctmat1_blocks !tens_block_mx !tens_row_mx !tens_col_mx. rewrite [-1]mx11_scalar !mxE /= !tens_scalar_mx !tens0mx scaleNr !scale1r. apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. rewrite !castmx_comp !esymK /=. rewrite !(castmx_block (mul1n _) (mul1n _) (mul2n _) (mul2n _)). rewrite !castmx_comp !castmx_id /=. rewrite !(castmx_row (mul1n _) (mul1n _)). rewrite !(castmx_block (mul1n _) (mul1n _) (mul1n _) (mul1n _)) /=. rewrite !(castmx_col (mul1n _) (mul1n _)) !castmx_comp !castmx_id /=. by rewrite !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)