Assume Heq: rational_numbers = setprod R R.

We will prove False.

Apply setprod_R_R_neq_rational_numbers to the current goal.

rewrite the current goal using Heq (from right to left).

Use reflexivity.

∎