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