Assume Heq: rational_numbers = R.

We will prove False.

Apply R_neq_rational_numbers to the current goal.

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

Use reflexivity.

∎