proposition: Lemma Qle_is_not_lt : forall x y : Q, x <= y <-> ~ y < x.
proof: Proof. firstorder using Qle_not_lt, Qnot_lt_le. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q