proposition: Lemma Qle_dec:forall (x y:Q), {Qle x y}+{~(Qle x y)}.
proof: Proof. intros x y. case (Q_le_lt_dec x y); intros; [ left | right ] ; trivial. intros H'; apply H'; trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)