proposition: Lemma Qle_lt_eq_dec : forall x y : Q, Qle x y -> {Qlt x y} + {x = y}.
proof: Proof. intros [| x| x] [| y| y] Hxy; try solve [ right; reflexivity | left; auto with * | right; auto with * | apply False_rec; apply Hxy; auto with * ]; [ generalize (Qle_Qpositive_le_pos _ _ Hxy) | generalize (Qle_Qpositive_le_neg _ _ Hxy) ]; clear Hxy; intro Hxy; match goal with | id1:(Qpositive_le ?X1 ?X2) |- _ => case (Qpositive_le_dec X2 X1); intro H; [ right; apply f_equal with Qpositive; apply Qpositive_le_antisym; assumption | left; constructor; assumption ] end. Qed.
imports: Coq(FunInd) QArithSternBrocot(Field_Theory_Q)