proposition: Lemma preserve_pos_meval n (m : monom n) : preserv pos (meval m).
proof: Proof. intros v Hv. rewrite (Vmap_proj1_sig Hv). apply pos_meval. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)