proposition: Lemma arctic_mult_notInf a b : a <> MinusInfBZ -> b <> MinusInfBZ -> Amult a b <> MinusInfBZ.
proof: Proof. destruct a; auto. destruct b; auto. discr. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)