Let x be given.

Assume Hx.

Let y be given.

Assume Hy.

Apply diadic_rational_p_SNoS_omega to the current goal.

Apply mul_SNo_diadic_rational_p to the current goal.

Apply SNoS_omega_diadic_rational_p to the current goal.

An exact proof term for the current goal is Hx.

Apply SNoS_omega_diadic_rational_p to the current goal.

An exact proof term for the current goal is Hy.

∎