proposition: Lemma coef_pos_power : forall k n (p : poly n), coef_pos p -> coef_pos (ppower p k).
proof: Proof. induction k; intros; simpl. intuition. apply coef_pos_mult. hyp. apply IHk. hyp. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)