proposition: Lemma Qtrichotomy_inf:forall x y,{Qlt x y}+{x=y}+{Qlt y x}.
proof: Proof. intros x y. case (Q_le_lt_dec x y); intros H; [ case (Qle_lt_eq_dec x y H); intros H0; left;[left|right] | right ]; trivial. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)