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