proposition: Lemma pos_peval : forall n (p : poly n) v, coef_pos p -> 0 <= peval p (vals v).
proof: Proof. induction p; intros; simpl. lia. destruct a. simpl in H. destruct H. apply Zplus_le_0_compat. apply Zmult_le_0_compat. hyp. apply pos_meval. apply IHp. hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)