proposition: Lemma coef_pos_mpmult : forall n c (m : monom n) (p : poly n), 0 <= c -> coef_pos p -> coef_pos (mpmult c m p).
proof: Proof. induction p; intros; simpl. exact I. destruct a. simpl. simpl in H0. destruct H0. split. apply Zmult_le_0_compat; hyp. apply IHp; hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)