proposition: Lemma peval_power : forall n (p : poly n) (k : nat) (v : vec n), peval (ppower p k) v = power (peval p v) k.
proof: Proof. induction k; intros; simpl. rewrite meval_one. ring. rewrite peval_mult, IHk. refl. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)