We will prove ¬ (two_by_nat_order_topology = discrete_topology two_by_nat).
Assume Heq: two_by_nat_order_topology = discrete_topology two_by_nat.
Set singleton_1_0 to be the term {(1,0)}.
We prove the intermediate claim Hsingleton_in_discrete: singleton_1_0 ∈ discrete_topology two_by_nat.
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Helem: (1,0) ∈ two_by_nat.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 1 0 In_1_2 H0omega).
We prove the intermediate claim Hsub: singleton_1_0 ⊆ two_by_nat.
Let y be given.
Assume Hy: y ∈ singleton_1_0.
We will prove y ∈ two_by_nat.
We prove the intermediate claim HyEq: y = (1,0).
An exact proof term for the current goal is (SingE (1,0) y Hy).
rewrite the current goal using HyEq (from left to right).
An exact proof term for the current goal is Helem.
An exact proof term for the current goal is (PowerI two_by_nat singleton_1_0 Hsub).
We prove the intermediate claim Hsingleton_in_order: singleton_1_0 ∈ two_by_nat_order_topology.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is Hsingleton_in_discrete.
An exact proof term for the current goal is (two_by_nat_singleton_not_open Hsingleton_in_order).
∎