proposition: Theorem Qplus_assoc_one_neg' : forall (n m : Q) (p' : Qpositive), Qplus n (Qplus m (Qneg p')) = Qplus (Qplus n m) (Qneg p').
proof: Proof. intros n m; case m. intros; try rewrite <- (Qplus_sym Zero); repeat rewrite Qplus_zero_left; auto with *. case n. 2: intros n' m' p'; apply Qplus_assoc_one_neg. intros m' p'; repeat rewrite Qplus_zero_left; auto. intros n' m' p'. repeat rewrite (Qplus_sym (Qneg n')). repeat rewrite <- Qplus_assoc_two_neg. repeat rewrite (Qplus_sym (Qneg n')). auto. intros m' p'; apply Qplus_assoc_two_neg. Qed.