proposition: Lemma coef_pos_app : forall n (p1 p2 : poly n), coef_pos (p1 ++ p2) -> coef_pos p1 /\ coef_pos p2.
proof: Proof. unfold coef_pos. intros n p1 p2. simpl. rewrite ListUtil.lforall_app. intuition. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)