proposition: Lemma fin_absolute_finite : forallb (fun f => babsolute_finite (trsInt f)) Fs = true -> forall f : sig, absolute_finite (trsInt f).
proof: Proof. rewrite forallb_forall. intros H f. rewrite <- babsolute_finite_ok. apply H. apply Fs_ok. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil Matrix AMonAlg AArcticBasedInt VecUtil OrdSemiRing SN RelUtil AMatrixBasedInt ListUtil)