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