proposition: Lemma coef_pos_pcomp : forall n k (p : poly n) (ps : vector (poly k) n), coef_pos p -> Vforall (@coef_pos k) ps -> coef_pos (pcomp p ps).
proof: Proof. induction p; intros; simpl. exact I. destruct a. simpl. simpl in H. destruct H. apply coef_pos_plus. apply coef_pos_cpmult. hyp. apply coef_pos_mcomp. hyp. apply IHp; hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)