proposition: Lemma tvec_cvec z sq : tvec z sq = (cvec z sq) *m (ctmat (size sq)).
proof: Proof. elim: sq z => [|q sq ihsq] z /=. rewrite mulmx1; apply/rowP=> [] [i hi] /=; rewrite !mxE /=. move: hi; rewrite expn0 ltnS leqn0; move/eqP=> -> /=. rewrite /poly_comb big_ord0 /taq /constraints /=. rewrite sumMz; apply: (congr_big)=> //= x _. by rewrite hornerC sgz1 big_ord0. rewrite /ctmat /ntensmx /=. case: sq ihsq=> /= [|q' sq] ihsq; first by apply: tvec_cvec1. rewrite cvec_rec tensmx_decl mulmxA tvec_rec. apply/eqP; rewrite (can2_eq (castmxK _ _) (castmxKV _ _)); apply/eqP. rewrite !castmx_mul !castmx_id [row_mx _ _ *m _]mulmx_cast. congr (_ *m _); last by congr (castmx (_, _) _); apply: nat_irrelevance. rewrite /=; have->: forall n, exp3S n.+1 = mul3n (3^n.+1)%N. by move=> n; apply: nat_irrelevance. by rewrite mul_1tensmx !ihsq. 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)