proposition: Theorem Qplus_assoc_one_neg : forall n' m' p' : Qpositive, Qplus (Qpos n') (Qplus (Qpos m') (Qneg p')) = Qplus (Qplus (Qpos n') (Qpos m')) (Qneg p').
proof: Proof. simpl in |- *; intros n' m' p'. Case' (Qpositive_le_dec m' p'). intros Hle; case (Qpositive_eq_dec m' p'). intros Heq; Case' (Qpositive_le_dec (Qpositive_plus n' m') p'). intros Hle1. elim (Qpositive_plus_diff p' n'). apply Qpositive_le_antisym. apply Qpositive_plus_le. generalize Hle1; rewrite Heq; rewrite Qpositive_plus_sym; auto. intros H H0 H1; rewrite <- Heq. rewrite Qpositive_sub_correct; auto. Case' (Qpositive_le_dec n' (Qpositive_sub p' m')). case (Qpositive_eq_dec n' (Qpositive_sub p' m')). intros e q n0; Case' (Qpositive_le_dec (Qpositive_plus n' m') p'). case (Qpositive_eq_dec (Qpositive_plus n' m') p'). auto. intros n1 q0. elim n1; rewrite e. rewrite Qpositive_sub_correct2; auto. intros Hnot1 Hle' Hnot; elim Hnot; rewrite e. rewrite Qpositive_sub_correct2; auto. apply Qpositive_le_refl. Case' (Qpositive_le_dec (Qpositive_plus n' m') p'). case (Qpositive_eq_dec (Qpositive_plus n' m') p'). intros e q n0 q0 n1. elim n0. rewrite <- e. rewrite Qpositive_sub_correct; auto. intros e q n0 q0 n1. rewrite Qpositive_sub_sub_assoc_l; auto. rewrite Qpositive_plus_sym; auto. rewrite Qpositive_plus_sym; auto. rewrite <- (Qpositive_sub_correct2 p' m'); auto. rewrite (Qpositive_plus_sym m'); apply Qpositive_le_add; auto with *. intros H H0 H1 n0 q n1. elim n0; apply Qpositive_le_antisym; auto. rewrite <- (Qpositive_sub_correct n' m'). apply Qpositive_le_sub_r; auto. rewrite Qpositive_plus_sym; apply sym_not_equal; apply Qpositive_plus_diff. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. Case' (Qpositive_le_dec (Qpositive_plus n' m') p'). case (Qpositive_eq_dec (Qpositive_plus n' m') p'). intros e q H H0 H1 n0. elim H1; rewrite <- e; rewrite Qpositive_sub_correct; apply Qpositive_le_refl. intros n0 q H H0 H1 n1. elim H1. rewrite <- (Qpositive_sub_correct n' m'). apply Qpositive_le_sub_r; auto with *. apply sym_not_equal; rewrite Qpositive_plus_sym; apply Qpositive_plus_diff. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. intros H H0 H3 H1 H2 H4 n0. rewrite Qpositive_sub_sub_assoc; auto with *. Case' (Qpositive_le_dec (Qpositive_plus n' m') p'). case (Qpositive_eq_dec (Qpositive_plus n' m') p'). intros e q H H0 H1. elim H1. rewrite <- e; rewrite Qpositive_plus_sym; apply Qpositive_plus_le. intros n0 q H H0 H1. elim H1. apply Qpositive_le_trans with (Qpositive_plus n' m'); auto. rewrite Qpositive_plus_sym; apply Qpositive_plus_le. intros H H0 H3 H1 H2 H4. rewrite Qpositive_plus_sym. rewrite Qpositive_plus_sub_assoc; auto with *. rewrite Qpositive_plus_sym; auto. Qed.