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