proposition: Theorem Qpositive_mult_assoc : forall w w' w'' : Qpositive, Qpositive_mult (Qpositive_mult w w') w'' = Qpositive_mult w (Qpositive_mult 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_mult in |- *. rewrite Heq; rewrite Heq'; rewrite Heq''. elim (construct_correct2' (S p * S p' + S q * S q') (S p * S p') (S q * S q')). intros d; elim (interp_non_zero (Qpositive_c (S p * S p') (S q * S q') (S p * S p' + 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 p'' + S q' * S q'') (S p' * S p'') (S q' * S q'')). intros d'; elim (interp_non_zero (Qpositive_c (S p' * S p'') (S q' * S q'') (S p' * S p'' + 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 fst, snd in Heq1, Heq2, Heq4, Heq5. apply mult_reg_l with d'. rewrite (Nat.mul_comm (S p * S p4)). repeat rewrite (Nat.mul_comm (S d')); repeat rewrite <- Nat.mul_assoc; rewrite <- Heq4; rewrite <- Heq5. clear Heq4 Heq5 Heq6. apply mult_reg_l with 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.