proposition: Lemma fin_monotone_succ : forallb (fun f => bpstrong_monotone (trsInt f)) Fs = true -> AWFMInterpretation.monotone I succ.
proof: Proof. intro H. apply monotone_succ. intro f. rewrite <- bpstrong_monotone_ok. rewrite forallb_forall in H. apply H. apply Fs_ok. Qed.
imports: CoLoR(APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs MonotonePolynom LogicUtil BoolUtil)