Let n be given.
Assume HnZ.
We prove the intermediate claim HnOmega: n ∈ ω.
An exact proof term for the current goal is (Zplus_mem_omega n HnZ).
We prove the intermediate claim HnNat: nat_p n.
An exact proof term for the current goal is (omega_nat_p n HnOmega).
We prove the intermediate claim HnNeq0: n ≠ 0.
An exact proof term for the current goal is (Zplus_mem_nonzero n HnZ).
We prove the intermediate claim Hcase: n = 0 ∨ ∃m : set, nat_p m ∧ n = ordsucc m.
An exact proof term for the current goal is (nat_inv n HnNat).
Apply (Hcase ({n} ∈ order_topology_basis Zplus)) to the current goal.
Assume Hn0: n = 0.
We will prove {n} ∈ order_topology_basis Zplus.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnNeq0 Hn0).
Assume Hex: ∃m : set, nat_p m ∧ n = ordsucc m.
Apply Hex to the current goal.
Let m be given.
Assume Hmpair.
Apply Hmpair to the current goal.
Assume HmNat HnEq.
Apply (xm (m = 0)) to the current goal.
Assume Hm0: m = 0.
We will prove {n} ∈ order_topology_basis Zplus.
rewrite the current goal using HnEq (from left to right).
rewrite the current goal using Hm0 (from left to right).
An exact proof term for the current goal is singleton_ordsucc0_in_order_topology_basis_Zplus.
Assume HmNe0: m ≠ 0.
We will prove {n} ∈ order_topology_basis Zplus.
We prove the intermediate claim HmZ: m ∈ Zplus.
An exact proof term for the current goal is (nat_nonzero_in_Zplus m HmNat HmNe0).
rewrite the current goal using HnEq (from left to right).
An exact proof term for the current goal is (singleton_ordsucc_in_order_topology_basis_Zplus m HmZ).
∎