proposition: Lemma tvec_cvec1 z q : tvec z [::q] = (cvec z [::q]) *m ctmat1.
proof: Proof. apply/rowP => j. rewrite /tvec !mxE /poly_comb /= !big_ord_recl !big_ord0 //=. rewrite !(expr0,expr1,mulr1) /=. case: j=> [] [|[|[|j]]] hj //. * by rewrite !mxE /= mulr0 add0r mulr1 mulrN1 addr0 taq_constraint1. * by rewrite !mxE /= mulr0 !mulr1 add0r addr0 taq_constraint2. * by rewrite !mxE /= addrA (@taq_constraint0 _ q) !mulr1 addr0 -addrA addrC. 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)