proposition: Lemma defaultPoly_wm n : pweak_monotone (defaultPoly n).
proof: Proof. Proof with simpl; auto with zarith. intros. split... apply lforall_intro. intros. ded (in_list_of_vec H). ded (Vbuild_in (fun i ip => (1%Z, mxi ip)) x H0). decomp H1. subst... Qed.
imports: Coq(Program) CoLoR(ListUtil LogicUtil ZUtil VecUtil Problem ATrs SN APolyInt Polynom RelUtil MonotonePolynom PositivePolynom NaryFunction MonAlgChecker IntBasedChecker Proof OptUtil AWFMInterpretation)