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