proposition: Lemma Qlt_is_antisymmetric_unfolded : forall x y : Q, (x<y) -> Not (y<x).
proof: Proof. intros x y E1 E2. apply (Qlt_irrefl x). eapply Qlt_trans; eauto. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q