proposition: Lemma preserve_pos_peval : forall n (p : poly n), coef_pos p -> preserv pos (peval p).
proof: Proof. intros. unfold preserv. intros v Hv. rewrite (Vmap_proj1_sig Hv). apply pos_peval. hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)