We will prove order_topology ω = discrete_topology ω.

An exact proof term for the current goal is omega_order_topology_is_discrete.

∎