proposition: Theorem Qgt_trans : forall x y z : Q, Qgt x y -> Qgt y z -> Qgt x z.
proof: Proof. intros x y z H; elim H; auto with *. intros x' y' H1 H2; inversion H2; auto with *. apply Qgt_pos_pos. red in |- *; intros H5; elim H3. apply Qpositive_le_trans with x'; auto with *. apply not_Qpositive_le_Qpositive_le'. auto. intros x' y' H1 H2; inversion H2; auto with *. apply Qgt_neg_neg. red in |- *; intros H5; elim H3. apply Qpositive_le_trans with x'; auto with *. apply not_Qpositive_le_Qpositive_le'. auto. intros x' H1; inversion H1; auto with *. intros x' y' H1; inversion H1; auto with *. intros x' H1; inversion H1; auto. Qed.