proposition: Lemma fin_PolyWeakMonotone : forallb (fun f => bpweak_monotone (PI f)) Fs = true -> PolyWeakMonotone.
proof: Proof. rewrite forallb_forall. intros H f. rewrite <- bpweak_monotone_ok. apply H. apply Fs_ok. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)