proposition: Lemma peval_mult : forall n (p1 p2 : poly n) (v : vec n), peval (p1 * p2) v = peval p1 v * peval p2 v.
proof: Proof. induction p1; intros; simpl. refl. destruct a. simpl. rewrite peval_plus, peval_mpmult, IHp1. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)