proposition: Lemma peval_mpplus : forall n c (m : monom n) (p : poly n) (v : vec n), peval (mpplus c m p) v = c * meval m v + peval p v.
proof: Proof. intros. elim p. auto. intros (c',m'). intros. simpl. case (monom_eq_dec m m'); simpl; intro. subst m'. ring. rewrite H. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)