proposition: Lemma coef_pos_plus : forall n (p1 p2 : poly n), coef_pos p1 -> coef_pos p2 -> coef_pos (p1 + p2).
proof: Proof. induction p1; intros; simpl. hyp. destruct a. simpl in H. destruct H. apply coef_pos_mpplus. hyp. apply IHp1; hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)