proposition: Lemma plus_inf_dec : forall m n, { exists p, (m = Fin p \/ n = Fin p) /\ m + n = Fin p} + { m + n = MinusInfBZ /\ m = MinusInfBZ /\ n = MinusInfBZ }.
proof: Proof. intros. destruct m. left. destruct n. exists (Z.max z z0). split. apply Z.max_case; auto. trivial. exists z. auto. destruct n. left. exists z. auto. right. auto. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)