Let m be given.

Assume Hm.

Apply int_diadic_rational_p to the current goal.

Apply Subq_omega_int to the current goal.

An exact proof term for the current goal is Hm.

∎