proposition: Lemma ap_Q_cotransitive0 : forall x y : Q, (x/=y) -> forall z : Q, (x/=z) or (z/=y).
proof: Proof. intros x y X z. unfold Qap in |- *. case (Qeq_dec x z). intro e. right. red in |- *. intro H0. apply X. exact (Qeq_trans x z y e H0). intros n. left. intro H. elim n. auto. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q