proposition: Lemma mult_inf_dec : forall m n, { exists mi, exists ni, m = TPos mi /\ n = TPos ni /\ m * n = TPos (mi + ni) } + { m * n = PlusInf /\ (m = PlusInf \/ n = PlusInf) }.
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)