proposition: Lemma defaultPoly_sm n : pstrong_monotone (defaultPoly n).
proof: Proof. split. apply defaultPoly_wm. intros. assert (HH : List.In (1%Z, mxi H) (defaultPoly n)). apply defaultPoly_mxi_1. set (w := coefPos_geC (defaultPoly n) (mxi H) 1 (defaultPoly_wm n) HH). auto with zarith. Qed.
imports: Coq(Program) CoLoR(ListUtil LogicUtil ZUtil VecUtil Problem ATrs SN APolyInt Polynom RelUtil MonotonePolynom PositivePolynom NaryFunction MonAlgChecker IntBasedChecker Proof OptUtil AWFMInterpretation)