proposition: Lemma Qlt_gives_apartness : forall x y : Q, Iff (x/=y) ((x<y) or (y<x)).
proof: Proof. Proof with intuition. intros x y; split; intros E. destruct (Q_dec x y)... destruct E. apply Qlt_not_eq... apply Qnot_eq_sym, Qlt_not_eq... Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q