Apply int_SNo_cases to the current goal.
Let n be given.
Assume Hn.
We will prove - n ∈ int.
Apply int_minus_SNo_omega to the current goal.
An exact proof term for the current goal is Hn.
Let n be given.
Assume Hn.
We will prove - - n ∈ int.
rewrite the current goal using minus_SNo_invol n (ordinal_SNo n (nat_p_ordinal n (omega_nat_p n Hn))) (from left to right).
We will prove n ∈ int.
Apply Subq_omega_int to the current goal.
An exact proof term for the current goal is Hn.
∎