proposition: Lemma ZFap_tight : forall n : Z, tight_apart (ZFeq n) (ZFap n).
proof: Proof. unfold tight_apart in |- *. unfold ZFap in |- *. unfold ZFeq in |- *. intros n x y. case x. case y. intros x0 H0 H0'x1 H1 H1'. red in |- *. unfold not in |- *. unfold Not in |- *. intuition. Qed.
imports: Coq.ZArith.ZArith CoRN.algebra.CSetoids