proposition: Lemma bcoef_pos_ok n (p : poly n) : bcoef_pos p = true <-> coef_pos p.
proof: Proof. apply ListUtil.forallb_lforall. intros [z m]. apply is_not_neg_ok. Qed.
imports: CoLoR(Polynom ZUtil LogicUtil NaryFunction VecUtil) Coq(List Lia)