proposition: Theorem Qgt_total : forall x y : Q, Qgt x y \/ x = y \/ Qgt y x.
proof: Proof. intros x y; case y; case x; auto. intros x' y'; case (Qpositive_le_dec x' y'); auto with *. case (Qpositive_eq_dec x' y'). intros e q; right; left; rewrite e; auto. intros n q; right; right; apply Qgt_pos_pos. red in |- *; intros H; elim n; apply Qpositive_le_antisym; auto. intros x' y'; case (Qpositive_le_dec x' y'); auto with *. case (Qpositive_eq_dec x' y'). intros e q; right; left; rewrite e; auto. intros n q; left; apply Qgt_neg_neg. red in |- *; intros H; elim n; apply Qpositive_le_antisym; auto. Qed.