proposition: Lemma ctmat1_unit : zmxR ctmat1 \in unitmx.
proof: Proof. rewrite /mem /in_mem /= /unitmx det_map_mx //. by rewrite det_ctmat1 unitfE intr_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)