proposition: Lemma meval_app : forall n1 (m1 : monom n1) (v1 : vec n1) n2 (m2 : monom n2) (v2 : vec n2), meval (Vapp m1 m2) (Vapp v1 v2) = meval m1 v1 * meval m2 v2.
proof: Proof. induction m1. intros. VOtac. simpl. apply zeqr. intros. VSntac v1. simpl. rewrite IHm1. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)