proposition: Lemma coefPos_ge0 : forall n (p : poly n) (m : monom n), coef_pos p -> coef m p >= 0.
proof: Proof. Proof with auto with zarith. induction p. simpl... intros. destruct a. simpl. destruct (monom_eq_dec m t). subst m. apply Zge_trans with (coef t p). destruct H. simpl in H... apply IHp. destruct H... apply IHp. destruct H... Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)