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