proposition: Lemma peval_mcomp : forall n k (m : monom n) (ps : vector (poly k) n) (v : vec k), peval (mcomp m ps) v = meval m (Vmap (fun p => peval p v) ps).
proof: Proof. induction n; intros. VOtac. simpl. rewrite zeql, meval_one. ring. VSntac m. VSntac ps. simpl. rewrite peval_mult, peval_power, IHn. refl. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)