proposition: Lemma pweak_monotone_default : PolyWeakMonotone default_pi.
proof: Proof. intro f. unfold pweak_monotone, coef_pos, default_pi. rewrite lforall_eq. intros. destruct (in_map_elim H). destruct H0. subst. simpl. lia. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)