proposition: Lemma peval_mpmult : forall n c (m : monom n) (p : poly n) (v : vec n), peval (mpmult c m p) v = c * meval m v * peval p v.
proof: Proof. induction p; intros; simpl. ring. destruct a. simpl. rewrite IHp, meval_mult. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)