proposition: Lemma bmonotone_interpretation_ok : forall n (fi : matrixInt dim n), bmonotone_interpretation fi = true <-> monotone_interpretation fi.
proof: Proof. intros. apply bVforall_ok. intro. apply bgt_nat_ok. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)