proposition: Lemma beq_ArcticDom_ok : forall x y, beq_ArcticDom x y = true <-> x = y.
proof: Proof. unfold beq_ArcticDom. destruct x; destruct y; simpl; try (intuition; discr). rewrite beq_nat_ok. intuition. 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)