proposition: Lemma ap_Z_tight0 : forall x y : Z, Not (x{#Z}y) <-> x = y.
proof: Proof. intros x y. red in |- *. split. unfold ap_Z in |- *. intro H. case (Z.eq_dec x y). intro e. assumption. contradiction. unfold ap_Z, Not. contradiction. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid