proposition: Lemma ZFap_cotransitive : forall n : Z, cotransitive (ZFap n).
proof: Proof. intro n. unfold cotransitive in |- *. unfold ZFap in |- *. intros x y. case x. case y. intros x0 H0 H0' x1 H1 H1' H2 z. case z. intros x2 H H'. set (H5 := Z.eq_dec x2 x1) in *. elim H5. clear H5. intro H5. right. rewrite H5. exact H2. clear H5. intro H5. left. exact H5. Qed.
imports: Coq.ZArith.ZArith CoRN.algebra.CSetoids