proposition: Lemma babsolute_finite_ok : forall n (fi : matrixInt dim n), babsolute_finite fi = true <-> absolute_finite fi.
proof: Proof. intros. unfold babsolute_finite, absolute_finite. rewrite is_above_zero_ok. tauto. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil Matrix AMonAlg AArcticBasedInt VecUtil OrdSemiRing SN RelUtil AMatrixBasedInt ListUtil)