proposition: Lemma fin_monotone_succ : forallb (fun f => bmonotone_interpretation (trsInt f)) Fs = true -> monotone I succ.
proof: Proof. intro H. apply monotone_succ. intro f. rewrite <- bmonotone_interpretation_ok. rewrite forallb_forall in H. apply H. apply Fs_ok. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)