proposition: Lemma fin_somewhere_tfinite : forallb (fun f => bsomewhere_tfinite (trsInt f)) Fs = true -> forall f : sig, somewhere_tfinite (trsInt f).
proof: Proof. rewrite forallb_forall. intros H f. rewrite <- bsomewhere_tfinite_ok. apply H. apply Fs_ok. Qed.
imports: CoLoR(ATropicalBasedInt Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil NatUtil AWFMInterpretation LogicUtil AMatrixBasedInt BoolUtil ListUtil) Coq(Structures.Equalities)