proposition: Lemma tropical_is_finite_ok v : tropical_is_finite v = true <-> v <> PlusInf.
proof: Proof. destruct v; simpl; intuition. discr. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)