proposition: Lemma coef_pos_cons : forall n c (m : monom n) (p : poly n), coef_pos ((c,m)::p) -> 0 <= c /\ coef_pos p.
proof: Proof. unfold coef_pos. intros n c m p. simpl. auto. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)