proposition: Lemma coef_pos_cpmult : forall n c (p : poly n), 0 <= c -> coef_pos p -> coef_pos (cpmult c p).
proof: Proof. induction p; intros; simpl. exact I. destruct a. simpl. simpl in H0. intuition. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)