proposition: Lemma bsomewhere_tfinite_ok : forall n (fi : matrixInt dim n), bsomewhere_tfinite fi = true <-> somewhere_tfinite fi.
proof: Proof. intros. unfold bsomewhere_tfinite, somewhere_tfinite. rewrite orb_eq, tropical_is_finite_ok, bVexists_ok. refl. intro. apply tropical_is_finite_ok. Qed.
imports: CoLoR(ATropicalBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil) Coq(Structures.Equalities)