proposition: Lemma peval_comp : forall n k (p : poly n) (ps : vector (poly k) n) (v : vec k), peval (pcomp p ps) v = peval p (Vmap (fun p => peval p v) ps).
proof: Proof. induction p; intros; simpl. refl. destruct a. rewrite peval_plus, peval_cpmult, IHp, peval_mcomp. refl. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)