proposition: Lemma ctmat_unit : forall n, zmxR (ctmat n) \in unitmx.
proof: Proof. case=> [|n] /=; first by rewrite map_mx1 ?unitmx1//; apply: zinjR_morph. elim: n=> [|n ihn] /=; first by apply: ctmat1_unit. rewrite map_mxT //. apply: tensmx_unit=> //; last exact: ctmat1_unit. by elim: n {ihn}=> // n ihn; rewrite muln_eq0. 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)