proposition: Lemma ctmat1_blocks : ctmat1 = (block_mx 1 (row_mx 1 1) (col_mx (-1) 0) (block_mx 1 1 0 1 : 'M_(1+1)%N)).
proof: Proof. apply/matrixP=> i j; rewrite !mxE. by do 4?[case: splitP => ?; rewrite !mxE ?ord1=> ->]. 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)