We will prove order_topology Zplus = discrete_topology Zplus.

An exact proof term for the current goal is Zplus_order_topology_is_discrete.

∎