Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

We will prove x * recip_SNo y ∈ real.

Apply real_mul_SNo to the current goal.

An exact proof term for the current goal is Hx.

Apply real_recip_SNo to the current goal.

An exact proof term for the current goal is Hy.

∎