proposition: Lemma mult_inf_dec : forall m n, { exists mi, exists ni, m = Pos mi /\ n = Pos ni /\ m * n = Pos (mi + ni) } + { m * n = MinusInf /\ (m = MinusInf \/ n = MinusInf) }.
proof: Proof. intros. destruct m. destruct n. left. exists n0. exists n. repeat split. right. auto. right. auto. Qed.
imports: Coq(Morphisms) CoLoR(RelDec RelUtil SN RelExtras NatUtil LogicUtil ZUtil)