proposition: Lemma ap_Z_cotransitive0 : forall x y : Z, (x{#Z}y) -> forall z : Z, (x{#Z}z) or (z{#Z}y).
proof: Proof. intros x y X z. unfold ap_Z in |- *. case (Z.eq_dec x z). intro e. right. rewrite <- e. assumption. intro n. left. assumption. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid