proposition: Lemma tropical_plus_notInf_left a b : a <> PlusInf -> Aplus a b <> PlusInf.
proof: Proof. destruct a. destruct b; discr. auto. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)