Record ZF (n:Z):Set:=
{ZF_crr:> Z ;
ZF_prf0: (Zlt ZF_crr n);
ZF_prf1: (Zle 0 ZF_crr)
}.

Definition ZFeq (n : Z) : ZF n -> ZF n -> Prop.
Defined.

Definition ZFap (n : Z) : ZF n -> ZF n -> CProp.
Defined.

Lemma ZFap_irreflexive : forall n : Z, irreflexive (ZFap n).

Lemma ZFap_symmetric : forall n : Z, Csymmetric (ZFap n).

Lemma ZFap_cotransitive : forall n : Z, cotransitive (ZFap n).

Lemma ZFap_tight : forall n : Z, tight_apart (ZFeq n) (ZFap n).

Definition Zless (n : Z) :=
  Build_is_CSetoid (ZF n) (ZFeq n) (ZFap n) (ZFap_irreflexive n)
    (ZFap_symmetric n) (ZFap_cotransitive n) (ZFap_tight n).

Definition ZCSetoid_of_less (n : Z) : CSetoid :=
  Build_CSetoid (ZF n) (ZFeq n) (ZFap n) (Zless n).