proposition: Lemma coef_pos_coef : forall n (p : poly n) m, coef_pos p -> 0 <= coef m p.
proof: Proof. induction p; intros; simpl. lia. destruct a. simpl in H. destruct H. case (monom_eq_dec m t); intro. assert (0 <= coef m p). apply IHp. hyp. lia. apply IHp. hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)