proposition: Lemma peval_app : forall n (p1 p2 : poly n) (v : vec n), peval (p1 ++ p2) v = peval p1 v + peval p2 v.
proof: Proof. intros. elim p1. auto. intros (c,m). intros. simpl. rewrite H. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)