proposition: Theorem Qgt_antisym : forall x y : Q, Qgt x y -> ~ Qgt y x.
proof: Proof. intros x y H; elim H. intros x' y' H1; red in |- *; intros H2; elim H1. inversion H2. apply not_Qpositive_le_Qpositive_le'; auto with *. intros x' y' H1; red in |- *; intros H2; elim H1. inversion H2; apply not_Qpositive_le_Qpositive_le'; auto. unfold not in |- *; intros x' H1; inversion H1. unfold not in |- *; intros x' y' H1; inversion H1. unfold not in |- *; intros x' H1; inversion H1. Qed.