proposition: Lemma Qeq_le_def : forall x y, x == y <-> x <= y /\ y <= x.
proof: Proof. intros. split. intros H; rewrite -> H. firstorder using Qle_refl. firstorder using Qle_antisym. Qed.
imports: Coq.QArith.QArith_base CoRN.order.TotalOrder