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