proposition: Lemma taq_no_constraint z : taq z 1 = (constraints z [::] [::])%:~R.
proof: Proof. rewrite /constraints /taq !sumMz; apply: congr_big=> // x _. by rewrite hornerC sgz1 big_ord0. 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)