proposition: Lemma Q_le_lt_dec:forall (x y:Q), {Qle x y}+{Qlt y x}.
proof: Proof. intros [|x|x] [|y|y]; unfold Qle; try (right; trivial || fail). left; apply Qlt_irreflexive. left; apply Qpos_not_lt_Zero. apply Qlt_dec_Qpos. left; apply Zero_not_lt_Qneg. left; apply Qpos_not_lt_Qneg. apply Qlt_dec_Qneg. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)