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