proposition: Lemma beq_ArcticBZDom_ok x y : beq_ArcticBZDom x y = true <-> x = y.
proof: Proof. unfold beq_ArcticBZDom. destruct x; destruct y; simpl; try (intuition; discr). rewrite beq_Z_ok. intuition. subst. refl. inversion H. refl. Qed.
imports: Coq(Relations Arith Compare Bool Setoid Morphisms) CoLoR(RelDec LogicUtil RelExtras EqUtil NatUtil ZUtil) Bignums(BigN) Coq(ZArith) Bignums(BigZ) CoLoR(ZUtil)