proposition: Theorem Qplus_sym : forall a b : Q, Qplus a b = Qplus b a.
proof: Proof. intros a b; case a; case b; simpl in |- *; auto; try (intros a' b'; apply f_equal with (f := Qpos) || apply f_equal with (f := Qneg); apply Qpositive_plus_sym). intros b' a'; case (Qpositive_le_dec a' b'). case (Qpositive_eq_dec a' b'). case (Qpositive_le_dec b' a'). case (Qpositive_eq_dec b' a'). auto. intros H; intros; elim H; auto. intros H H1; intros; elim H; rewrite H1; apply Qpositive_le_refl. case (Qpositive_le_dec b' a'). case (Qpositive_eq_dec b' a'). intros H H1 H2; elim H2; auto. intros H; intros; elim H; apply Qpositive_le_antisym; auto. auto. case (Qpositive_le_dec b' a'). case (Qpositive_eq_dec b' a'). intros H H1 H2; elim H2; rewrite H; apply Qpositive_le_refl. auto. intros H1 H2; elim (Qpositive_le_total a' b'); intros H3; (elim H1; exact H3) || (elim H2; exact H3). intros b' a'; case (Qpositive_le_dec a' b'); case (Qpositive_le_dec b' a'). intros H H1; case (Qpositive_eq_dec a' b'). case (Qpositive_eq_dec b' a'); auto. intros H2 H3; elim H2; auto. intros H2; elim H2; apply Qpositive_le_antisym; auto. case (Qpositive_eq_dec a' b'); intros H H1 H2. elim H1; rewrite H; apply Qpositive_le_refl. auto. case (Qpositive_eq_dec b' a'). intros H H1 H2; elim H2; rewrite H; apply Qpositive_le_refl. auto. elim (Qpositive_le_total a' b'); intros H; repeat (intros Dummy; try (elim Dummy; auto; fail); clear Dummy). Qed.