proposition: Lemma ZFap_irreflexive : forall n : Z, irreflexive (ZFap n).
proof: Proof. unfold irreflexive in |- *. unfold ZFap in |- *. intros n x. case x. intuition. red in |- *. intuition. Qed.
imports: Coq.ZArith.ZArith CoRN.algebra.CSetoids