proposition: Theorem Qpositive_plus_assoc : forall w w' w'' : Qpositive, Qpositive_plus (Qpositive_plus w w') w'' = Qpositive_plus w (Qpositive_plus w' w'').
proof: Proof. intros w w' w''; elim (interp_non_zero w); intros p Hex; elim Hex; intros q Heq; clear Hex. elim (interp_non_zero w'); intros p' Hex; elim Hex; intros q' Heq'; clear Hex. elim (interp_non_zero w''); intros p'' Hex; elim Hex; intros q'' Heq''; clear Hex. unfold Qpositive_plus in |- *. rewrite Heq; rewrite Heq'; rewrite Heq''. elim (construct_correct2' (S p * S q' + S p' * S q + S q * S q') (S p * S q' + S p' * S q) (S q * S q')). intros d; elim (interp_non_zero (Qpositive_c (S p * S q' + S p' * S q) (S q * S q') (S p * S q' + S p' * S q + S q * S q'))); intros p3 Hex; elim Hex; intros q3 Heq3; rewrite Heq3; clear Hex. intros (Heq1, Heq2). elim (construct_correct2' (S p' * S q'' + S p'' * S q' + S q' * S q'') (S p' * S q'' + S p'' * S q') (S q' * S q'')). intros d'; elim (interp_non_zero (Qpositive_c (S p' * S q'' + S p'' * S q') (S q' * S q'') (S p' * S q'' + S p'' * S q' + S q' * S q''))); intros p4 Hex; elim Hex; intros q4 Heq6; rewrite Heq6; clear Hex. intros (Heq4, Heq5). apply construct_correct4'. simpl in |- *; auto with arith. simpl in |- *; auto with arith. simpl in |- *; auto with arith. simpl in |- *; auto with arith. auto. auto. unfold snd, fst in Heq5, Heq1, Heq2, Heq4, Heq5. apply mult_reg_l with d'. rewrite Nat.mul_add_distr_r. rewrite (Nat.mul_comm (S d')). rewrite Nat.mul_add_distr_r. repeat rewrite <- Nat.mul_assoc. rewrite <- Heq5. rewrite Nat.mul_add_distr_r. rewrite (Nat.mul_comm (S d')). rewrite Nat.mul_add_distr_r. rewrite (Nat.mul_comm (S p * S q4)). rewrite (Nat.mul_comm (S p4 * S q)). rewrite (Nat.mul_comm (S p4)). repeat rewrite <- Nat.mul_assoc. rewrite <- Heq5. rewrite <- Heq4. rewrite (Nat.mul_assoc (S p'')). rewrite <- (Nat.mul_comm (S q3)). rewrite <- Nat.mul_assoc. apply mult_reg_l with d. repeat rewrite (Nat.mul_comm (S d)); repeat rewrite Nat.mul_add_distr_r; repeat rewrite <- (Nat.mul_comm (S d)); repeat rewrite (Nat.mul_assoc (S d)); repeat rewrite (Nat.mul_comm (S d)); rewrite <- Heq1; rewrite <- Heq2. ring. simpl in |- *; auto with arith. simpl in |- *; auto with arith. auto. simpl in |- *; auto with arith. simpl in |- *; auto with arith. auto. Qed.