proposition: Lemma meval_mult : forall n (m1 m2 : monom n) (v : vec n), meval (mmult m1 m2) v = meval m1 v * meval m2 v.
proof: Proof. induction n; intros. VOtac. refl. VSntac m1. VSntac m2. simpl. unfold mmult in IHn. rewrite IHn, power_plus. ring. Qed.
imports: CoLoR(VecUtil LogicUtil NatUtil) Coq(Arith List Lia) CoLoR(ZUtil)