proposition: Lemma pos_meval : forall n (m : monom n) (v : vec n), 0 <= meval m (vals v).
proof: Proof. induction n; intros; simpl. lia. VSntac m. VSntac v. simpl. apply Zmult_le_0_compat. apply pos_power. destruct (Vhead v). hyp. apply IHn. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)