proposition: Theorem Qopp_plus : forall x y : Q, Qopp (Qplus x y) = Qplus (Qopp x) (Qopp y).
proof: Proof. intros x y. rewrite <- (Qplus_zero_left (Qplus (Qopp x) (Qopp y))). rewrite <- (Q_opp_def (Qplus x y)). rewrite (Qplus_sym (Qplus x y)). pattern (Qplus x y) at 3 in |- *; rewrite Qplus_sym. rewrite Qplus_assoc. rewrite Qplus_assoc. rewrite <- (fun a b : Q => Qplus_assoc a b (Qopp x)). rewrite Q_opp_def. rewrite <- (Qplus_sym Zero); rewrite Qplus_zero_left. rewrite <- Qplus_assoc; rewrite Q_opp_def. rewrite <- (Qplus_sym Zero); rewrite Qplus_zero_left. auto. Qed.