proposition: Theorem Qpositive_mult_distr : forall w w' w'' : Qpositive, Qpositive_mult (Qpositive_plus w w') w'' = Qpositive_plus (Qpositive_mult w 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, 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; intros (Heq1, Heq2); clear Hex. 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; intros (Heq4, Heq5); clear Hex. 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 p5 Hex; elim Hex; intros q5 Heq9; rewrite Heq9; intros (Heq7, Heq8); clear Hex. 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, Heq7, Heq8. apply mult_reg_l with d''. rewrite (Nat.mul_comm (S p5)). rewrite Nat.mul_add_distr_r. repeat (rewrite <- Nat.mul_assoc; try rewrite (Nat.mul_comm (S p5)); try rewrite (Nat.mul_comm (S q5))). repeat rewrite (Nat.mul_comm (S d'')); rewrite Nat.mul_add_distr_r; repeat rewrite <- Nat.mul_assoc; rewrite <- Heq7; rewrite <- Heq8. repeat (repeat rewrite (Nat.mul_comm (S p4)); repeat rewrite (Nat.mul_comm (S q4)); rewrite <- Nat.mul_assoc). apply mult_reg_l with d'; repeat rewrite (Nat.mul_comm (S d')); rewrite Nat.mul_add_distr_r; repeat rewrite <- Nat.mul_assoc. rewrite <- Heq4; rewrite <- Heq5. apply mult_reg_l with d; repeat rewrite (Nat.mul_comm (S d)); rewrite Nat.mul_add_distr_r; repeat rewrite (Nat.mul_comm (S q3)); rewrite (Nat.mul_comm (S p3)); repeat rewrite <- Nat.mul_assoc. 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. simpl in |- *; auto with arith. simpl in |- *; auto with arith. auto. Qed.