proposition: Lemma constraints1P (p : {poly R}) (sq : seq {poly R}) : (constraints (rootsR p) (sq) (nseq (size (sq)) 1))%:~R = ccount_weak p sq.
proof: Proof. rewrite constraints1_tvec; symmetry. rewrite castmxE mxE /= /ccount_weak. transitivity (\sum_(0 <= i < 3 ^ size sq) taqsR p sq i * coefs R (size sq) i). rewrite unlock /reducebig /= -foldr_map /= /index_iota subn0 foldr_map. elim: (3 ^ size sq)%N 0%R => [|n ihn] u //. by rewrite -[X in iota _ X]addn1 iotaD add0n /= foldr_cat ihn. rewrite big_mkord; apply: congr_big=> // i _. rewrite /taqsR /coefs /tvecR /=. have o : 'I_(3 ^ size sq) by rewrite exp3n; apply: ord0. rewrite (@nth_map _ o); last by rewrite size_enum_ord. by rewrite !castmxE !cast_ord_id !mxE /= nth_ord_enum taq_taqR. 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)