Apply int_SNo_cases to the current goal.
Let n be given.
Assume H1: n ∈ ω.
Assume H2: 0 ≤ n.
We will prove nat_p n.
An exact proof term for the current goal is omega_nat_p n H1.
Let n be given.
Assume H1: n ∈ ω.
Assume H2: 0 ≤ - n.
We will prove nat_p (- n).
We prove the intermediate claim LnS: SNo n.
An exact proof term for the current goal is omega_SNo n H1.
We prove the intermediate claim L1: n = 0.
Apply SNoLe_antisym n 0 LnS SNo_0 to the current goal.
We will prove n ≤ 0.
rewrite the current goal using minus_SNo_invol n LnS (from right to left).
rewrite the current goal using minus_SNo_0 (from right to left).
We will prove - - n ≤ - 0.
Apply minus_SNo_Le_contra 0 (- n) SNo_0 (SNo_minus_SNo n LnS) to the current goal.
We will prove 0 ≤ - n.
An exact proof term for the current goal is H2.
We will prove 0 ≤ n.
Apply ordinal_Subq_SNoLe 0 n ordinal_Empty (nat_p_ordinal n (omega_nat_p n H1)) to the current goal.
We will prove 0 ⊆ n.
Apply Subq_Empty to the current goal.
rewrite the current goal using L1 (from left to right).
rewrite the current goal using minus_SNo_0 (from left to right).
An exact proof term for the current goal is nat_0.
∎