proposition: Lemma taq_constraint2 z q : taq z (q ^+ 2) = (constraints z [::q] [:: 1])%:~R + (constraints z [::q] [::-1])%:~R.
proof: Proof. rewrite /constraints /taq !sumMz -big_split /=; apply: congr_big=> // x _. rewrite !big_ord_recl big_ord0 !muln1 /= horner_exp sgzX. by case: (sgzP q.[x])=> _. 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)