fact: Definition ctmat1 := \matrix_(i < 3, j < 3) (nth [::] [:: [:: 1%:Z ; 1 ; 1 ] ; [:: -1 ; 1 ; 1 ] ; [:: 0 ; 0 ; 1 ] ] i)`_j.
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)