proposition: Theorem Qpositive_le_plus_simpl : forall x y z : Qpositive, Qpositive_le (Qpositive_plus x z) (Qpositive_plus y z) -> Qpositive_le x y.
proof: Proof. intros x y z H; rewrite <- (Qpositive_sub_correct x z). rewrite <- (Qpositive_sub_correct y z). apply Qpositive_le_sub_r; auto with *. rewrite Qpositive_plus_sym; apply sym_not_equal; apply Qpositive_plus_diff. rewrite Qpositive_plus_sym; apply sym_not_equal; apply Qpositive_plus_diff. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. Qed.