proposition: Lemma Qle_dec x y: decision (Qle x y).
proof: Proof. intros. destruct (Qlt_le_dec y x); [right | left]; [apply Qlt_not_le |]; assumption. Defined.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax Coq.Classes.Morphisms CoRN.reals.fast.CRGroupOps CoRN.logic.Classic