proposition: Lemma det_ctmat1 : \det ctmat1 = 2.
proof: Proof. by do ?[rewrite (expand_det_row _ ord0) //=; rewrite ?(big_ord_recl,big_ord0) //= ?mxE //=; rewrite /cofactor /= ?(addn0, add0n, expr0, exprS); rewrite ?(mul1r,mulr1,mulN1r,mul0r,mul1r,addr0) /=; do ?rewrite [row' _ _]mx11_scalar det_scalar1 !mxE /=]. 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)