proposition: Lemma coef_pos_mcomp : forall k n (m : monom n) (ps : vector (poly k) n), Vforall (@coef_pos k) ps -> coef_pos (mcomp m ps).
proof: Proof. induction n; intros; simpl. intuition. VSntac ps. simpl. rewrite H0 in H. simpl in H. destruct H. apply coef_pos_mult. apply coef_pos_power. hyp. apply IHn. hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)