proposition: Lemma default_sm : forall f, poly_sm (buildSymInt (defaultIntForSymbol f)).
proof: Proof. intros. apply defaultPoly_sm. Qed.
imports: Coq(Program) CoLoR(ListUtil LogicUtil ZUtil VecUtil Problem ATrs SN APolyInt Polynom RelUtil MonotonePolynom PositivePolynom NaryFunction MonAlgChecker IntBasedChecker Proof OptUtil AWFMInterpretation)