fact: Definition bpstrong_monotone n (p : poly n) := bcoef_pos p && forallb (fun x => is_pos (coef (mxi (N_prf x)) p)) (L n).
imports: CoLoR(Polynom PositivePolynom NaryFunction VecUtil LogicUtil ListUtil ZUtil RelUtil NatUtil BoundNat) CoLoR(BoolUtil)