proposition: Lemma plus_inf_dec : forall m n, { exists p, (m = TPos p \/ n = TPos p) /\ m + n = TPos p} + { m + n = PlusInf /\ m = PlusInf /\ n = PlusInf }.
proof: Proof. intros. destruct m. left. destruct n. exists (min n0 n). split. apply Nat.min_case; auto. trivial. exists n0. auto. destruct n. left. exists n. auto. right. auto. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)