proposition: Lemma coef_pos_mpplus : forall n c (m : monom n) (p : poly n), 0 <= c -> coef_pos p -> coef_pos (mpplus c m p).
proof: Proof. induction p; intros; simpl. auto. destruct a. simpl in H0. destruct H0. case (monom_eq_dec m t); simpl; intuition. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)