proposition: Lemma tropical_plus_inf_max : forall x, x <> PlusInf -> PlusInf >> x.
proof: Proof. intros. destruct x. simpl. auto. exfalso. apply H. trivial. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)