fact: Definition Amult m n := match m, n with | MinusInfBZ, _ => MinusInfBZ | _, MinusInfBZ => MinusInfBZ | Fin m, Fin n => Fin (m + n) end.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)