proposition: Theorem Qplus_assoc_two_neg : forall (n : Q) (m' p' : Qpositive), Qplus n (Qplus (Qneg m') (Qneg p')) = Qplus (Qplus n (Qneg m')) (Qneg p').
proof: Proof. intros n; case n. intros; repeat rewrite Qplus_zero_left; auto. simpl in |- *; intros n' m' p'. Case' (Qpositive_le_dec n' (Qpositive_plus m' p')). case (Qpositive_eq_dec n' (Qpositive_plus m' p')). Case' (Qpositive_le_dec n' m'). case (Qpositive_eq_dec n' m'). intros e q e0; elim (Qpositive_plus_diff n' p'). pattern n' at 2 in |- *; rewrite e; auto. intros n0 q e q0; elim n0; apply Qpositive_le_antisym; auto. rewrite e; apply Qpositive_plus_le. intros H H0 H1 e q; simpl in |- *. Case' (Qpositive_le_dec (Qpositive_sub n' m') p'). case (Qpositive_eq_dec (Qpositive_sub n' m') p'); auto with *. rewrite e; intros H2; elim H2. rewrite Qpositive_plus_sym; rewrite Qpositive_sub_correct; auto. rewrite e; intros H2; elim H2. rewrite Qpositive_plus_sym; rewrite Qpositive_sub_correct; auto. Case' (Qpositive_le_dec n' m'). case (Qpositive_eq_dec n' m'). simpl in |- *. rewrite Qpositive_plus_sym. intros e q n0 q0; rewrite e; rewrite Qpositive_sub_correct; auto with *. simpl in |- *. intros; rewrite Qpositive_plus_sub_assoc; auto. simpl in |- *. Case' (Qpositive_le_dec (Qpositive_sub n' m') p'). case (Qpositive_eq_dec (Qpositive_sub n' m') p'). intros e q H H0 H1 n0 q0; elim n0. symmetry in |- *; apply add_sub_eq2; auto with *. intros; rewrite Qpositive_sub_sub_assoc; auto. rewrite Qpositive_plus_sym; auto. intros H H0 H3 H1 H2 H4 n0 q; elim H3. apply add_sub_le2; auto. Case' (Qpositive_le_dec n' m'). case (Qpositive_eq_dec n' m'). intros e q H H0 H1; elim H1; rewrite e; apply Qpositive_plus_le. simpl in |- *. intros n0 q H H0 H1; elim H1; apply Qpositive_le_trans with m'; auto with *. apply Qpositive_plus_le. simpl in |- *. Case' (Qpositive_le_dec (Qpositive_sub n' m') p'). case (Qpositive_eq_dec (Qpositive_sub n' m') p'). intros e q H H0 H2 H1; elim H1. symmetry in |- *; apply add_sub_eq2; auto with *. intros n0 q H H0 H3 H1 H2 H4; elim H4; apply add_sub_le1; auto with *. intros; rewrite Qpositive_sub_sub_assoc_l; auto with *. intros m' n' p'; simpl in |- *. rewrite Qpositive_plus_assoc; auto with *. Qed.