proposition: Lemma peval_minus n (p1 p2 : poly n) (v : vec n) : peval (p1 - p2) v = peval p1 v - peval p2 v.
proof: Proof. unfold pminus. rewrite peval_plus, peval_opp. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)