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