proposition: Lemma ap_Q_symmetric0 : forall x y : Q, (x/=y) -> y/=x.
proof: Proof. firstorder auto with crelations. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q