proposition: Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}.
proof: Proof. unfold Qlt, Qle; intros x y. exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)). Defined.
imports: ZArith_base ZArithRing ZArith.BinInt Morphisms Setoid Bool