fact: Fixpoint meval (n : nat) : monom n -> vec n -> Z := match n as n return monom n -> vec n -> Z with | O => fun _ _ => 1 | S _ => fun m v => power (Vhead v) (Vhead m) * meval (Vtail m) (Vtail v) end.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)