proposition: Theorem Qgt_plus : forall x y z : Q, Qgt x y -> Qgt (Qplus z x) (Qplus z y).
proof: Proof. intros x y z H; elim H. intros x' y' Hnle; generalize (not_Qpositive_le_Qpositive_le' _ _ Hnle). intros Hle; generalize (not_Qpositive_le_not_eq _ _ Hnle). intros Hneq. case z; simpl in |- *; auto. intros z'; apply Qgt_pos_pos. red in |- *; intros Hle'; elim Hneq; apply Qpositive_le_antisym. apply Qpositive_le_plus_simpl with z'; repeat rewrite <- (Qpositive_plus_sym z'); auto with *. auto. intros z'; Case' (Qpositive_le_dec z' x'). case (Qpositive_eq_dec z' x'). Case' (Qpositive_le_dec z' y'). intros q e q0. elim Hnle. rewrite <- e; auto. auto. Case' (Qpositive_le_dec z' y'). case (Qpositive_eq_dec z' y'). auto. intros n q n0 q0. apply Qgt_pos_pos. red in |- *; intros H0. elim Hnle; apply Qpositive_le_sub_simpl_r with z'; auto with *. auto. Case' (Qpositive_le_dec z' y'). intros q H0 H1 H2. elim Hneq; apply Qpositive_le_antisym; auto with *. apply Qpositive_le_trans with z'; auto. intros H0 H1 H4 H2 H3 H5. apply Qgt_neg_neg. red in |- *; intros H6. elim Hnle. apply Qpositive_le_sub_simpl_l with z'; auto. intros x' y' Hnle; case z; auto. simpl in |- *; auto. intros z'; simpl in |- *. Case' (Qpositive_le_dec z' x'). case (Qpositive_eq_dec z' x'). Case' (Qpositive_le_dec z' y'). case (Qpositive_eq_dec z' y'). intros e q e0 q0; elim Hnle; rewrite <- e; rewrite <- e0; apply Qpositive_le_refl. auto. intros H0 H1 H2 e q; elim Hnle; rewrite <- e; auto. Case' (Qpositive_le_dec z' y'). case (Qpositive_eq_dec z' y'). intros e q n q0; elim Hnle; rewrite <- e; try assumption. intros n q n0 q0. apply Qgt_neg_neg. red in |- *; intros H0. elim Hnle; apply Qpositive_le_sub_simpl_r with z'; auto with *. intros H0 H1 H2 n q; elim Hnle; apply Qpositive_le_trans with z'; auto. Case' (Qpositive_le_dec z' y'). case Qpositive_eq_dec; auto with *. intros H0 H1 H4 H2 H3 H5. apply Qgt_pos_pos. red in |- *; intros H6; elim Hnle. apply Qpositive_le_sub_simpl_l with z'; auto. simpl in |- *. intros z'; apply Qgt_neg_neg. red in |- *; intros H0; elim Hnle; apply Qpositive_le_plus_simpl with z'. repeat rewrite <- (Qpositive_plus_sym z'). auto. intros x'; case z. simpl in |- *; auto. intros z'; simpl in |- *. apply Qgt_pos_pos. red in |- *; intros H0; elim (Qpositive_plus_diff z' x'). apply Qpositive_le_antisym; auto. apply Qpositive_plus_le. intros z'; simpl in |- *. Case' (Qpositive_le_dec z' x'). case (Qpositive_eq_dec z' x'); auto with *. intros H0 H1 H2; apply Qgt_neg_neg. red in |- *; intros H3; elim (Qpositive_sub_diff z' x'); auto with *. apply Qpositive_le_antisym; auto. apply Qpositive_sub_le; auto. intros x' y'; case z; simpl in |- *; auto with *. intros z'; Case' (Qpositive_le_dec z' y'). case (Qpositive_eq_dec z' y'); auto with *. intros H0 H1 H2; apply Qgt_pos_pos. red in |- *; intros H3; elim (Qpositive_plus_diff z' x'). apply Qpositive_le_antisym. apply Qpositive_plus_le. apply Qpositive_le_trans with (Qpositive_sub z' y'); auto with *. apply Qpositive_sub_le; auto. intros z'; Case' (Qpositive_le_dec z' x'). case (Qpositive_eq_dec z' x'). auto. auto. intros H0 H1 H2; apply Qgt_neg_neg. red in |- *; intros H3; elim (Qpositive_plus_diff z' y'). apply Qpositive_le_antisym. apply Qpositive_plus_le. apply Qpositive_le_trans with (Qpositive_sub z' x'); auto with *. apply Qpositive_sub_le; auto. intros x'; case z; simpl in |- *. auto. intros z'; Case' (Qpositive_le_dec z' x'). case (Qpositive_eq_dec z' x'). auto. auto. intros H0 H1 H2; apply Qgt_pos_pos. red in |- *; intros H3; elim (Qpositive_sub_diff z' x'); auto. apply Qpositive_le_antisym; auto with *. apply Qpositive_sub_le; auto. intros z'; apply Qgt_neg_neg. red in |- *; intros H0; elim (Qpositive_plus_diff z' x'). apply Qpositive_le_antisym; auto. apply Qpositive_plus_le. Qed.