We will prove 1 ∈ K_set.
We prove the intermediate claim H1O: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim H1not0: 1 ∉ {0}.
Assume H10: 1 ∈ {0}.
We prove the intermediate claim Hbad: 1 = 0.
An exact proof term for the current goal is (SingE 0 1 H10).
An exact proof term for the current goal is (neq_1_0 Hbad).
We prove the intermediate claim H1In: 1 ∈ ω ∖ {0}.
An exact proof term for the current goal is (setminusI ω {0} 1 H1O H1not0).
We prove the intermediate claim Hinv1: inv_nat 1 ∈ K_set.
An exact proof term for the current goal is (ReplI (ω ∖ {0}) (λn0 : set ⇒ inv_nat n0) 1 H1In).
We prove the intermediate claim Hinv1eq: inv_nat 1 = 1.
We will prove inv_nat 1 = 1.
We prove the intermediate claim H1neq0: 1 ≠ 0.
An exact proof term for the current goal is neq_1_0.
We prove the intermediate claim Hmul: mul_SNo 1 (inv_nat 1) = 1.
An exact proof term for the current goal is (recip_SNo_invR 1 SNo_1 H1neq0).
rewrite the current goal using (mul_SNo_oneL (inv_nat 1) (SNo_recip_SNo 1 SNo_1)) (from right to left) at position 1.
An exact proof term for the current goal is Hmul.
rewrite the current goal using Hinv1eq (from right to left) at position 1.
An exact proof term for the current goal is Hinv1.
∎