Apply nat_complete_ind to the current goal.
Let n be given.
Assume Hn.
Assume IH: ∀m ∈ n, ∀x, SNo x → SNoLev x = m → diadic_rational_p x.
Let x be given.
Assume Hx: SNo x.
Assume Hxn: SNoLev x = n.
We will prove diadic_rational_p x.
Apply dneg to the current goal.
Assume HC: ¬ diadic_rational_p x.
We will prove False.
We prove the intermediate claim LxSo: x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ω.
rewrite the current goal using Hxn (from left to right).
An exact proof term for the current goal is nat_p_omega n Hn.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is Hx.
We prove the intermediate claim L1: ∃y, SNo_max_of (SNoL x) y.
Apply SNoS_omega_SNoL_max_exists x LxSo to the current goal.
Assume H1: SNoL x = 0.
We prove the intermediate claim L1a: ordinal (- x).
Apply SNo_max_ordinal (- x) (SNo_minus_SNo x Hx) to the current goal.
Let w be given.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
Assume Hw: w ∈ SNoS_ (SNoLev x).
We will prove w < - x.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x Hx) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLt_trichotomy_or_impred w (- x) ?? (SNo_minus_SNo x Hx) to the current goal.
Assume H2: w < - x.
An exact proof term for the current goal is H2.
Assume H2: w = - x.
We will prove False.
Apply In_irref (SNoLev w) to the current goal.
rewrite the current goal using H2 (from left to right) at position 2.
rewrite the current goal using minus_SNo_Lev x Hx (from left to right).
An exact proof term for the current goal is ??.
Assume H2: - x < w.
We will prove False.
Apply EmptyE (- w) to the current goal.
We will prove - w ∈ 0.
rewrite the current goal using H1 (from right to left).
We will prove - w ∈ SNoL x.
Apply SNoL_I x Hx (- w) (SNo_minus_SNo w ??) to the current goal.
We will prove SNoLev (- w) ∈ SNoLev x.
rewrite the current goal using minus_SNo_Lev w ?? (from left to right).
An exact proof term for the current goal is ??.
We will prove - w < x.
An exact proof term for the current goal is minus_SNo_Lt_contra1 x w Hx ?? ??.
We prove the intermediate claim L1b: - x = n.
rewrite the current goal using Hxn (from right to left).
We will prove - x = SNoLev x.
Use symmetry.
rewrite the current goal using minus_SNo_Lev x ?? (from right to left).
An exact proof term for the current goal is ordinal_SNoLev (- x) L1a.
We will prove False.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using minus_SNo_invol x ?? (from right to left).
We will prove diadic_rational_p (- - x).
Apply minus_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (- x).
rewrite the current goal using L1b (from left to right).
We will prove diadic_rational_p n.
Apply omega_diadic_rational_p to the current goal.
An exact proof term for the current goal is nat_p_omega n Hn.
Assume H1.
An exact proof term for the current goal is H1.
We prove the intermediate claim L2: ∃z, SNo_min_of (SNoR x) z.
Apply SNoS_omega_SNoR_min_exists x LxSo to the current goal.
Assume H1: SNoR x = 0.
We prove the intermediate claim L2a: ordinal x.
Apply SNo_max_ordinal x Hx to the current goal.
Let w be given.
Assume Hw: w ∈ SNoS_ (SNoLev x).
We will prove w < x.
Apply SNoS_E2 (SNoLev x) (SNoLev_ordinal x ??) w Hw to the current goal.
Assume Hw1 Hw2 Hw3 Hw4.
Apply SNoLt_trichotomy_or_impred w x ?? ?? to the current goal.
Assume H2: w < x.
An exact proof term for the current goal is H2.
Assume H2: w = x.
We will prove False.
Apply In_irref (SNoLev x) to the current goal.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is ??.
Assume H2: x < w.
We will prove False.
Apply EmptyE w to the current goal.
We will prove w ∈ 0.
rewrite the current goal using H1 (from right to left).
We will prove w ∈ SNoR x.
Apply SNoR_I x ?? w ?? ?? ?? to the current goal.
We prove the intermediate claim L2b: x = n.
rewrite the current goal using Hxn (from right to left).
We will prove x = SNoLev x.
Use symmetry.
An exact proof term for the current goal is ordinal_SNoLev x L2a.
We will prove False.
Apply HC to the current goal.
We will prove diadic_rational_p x.
Apply omega_diadic_rational_p to the current goal.
We will prove x ∈ ω.
rewrite the current goal using L2b (from left to right).
An exact proof term for the current goal is nat_p_omega n Hn.
Assume H1.
An exact proof term for the current goal is H1.
Apply L1 to the current goal.
Let y be given.
Assume Hy: SNo_max_of (SNoL x) y.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Assume Hy1: y ∈ SNoL x.
Assume Hy2: SNo y.
Assume Hy3: ∀w ∈ SNoL x, SNo w → w ≤ y.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume _ Hy1b Hy1c.
Apply L2 to the current goal.
Let z be given.
Assume Hz: SNo_min_of (SNoR x) z.
Apply Hz to the current goal.
Assume H.
Apply H to the current goal.
Assume Hz1: z ∈ SNoR x.
Assume Hz2: SNo z.
Assume Hz3: ∀w ∈ SNoR x, SNo w → z ≤ w.
Apply SNoR_E x Hx z Hz1 to the current goal.
Assume _ Hz1b Hz1c.
We prove the intermediate claim Lxx: SNo (x + x).
An exact proof term for the current goal is SNo_add_SNo x x Hx Hx.
We prove the intermediate claim Lyz: SNo (y + z).
An exact proof term for the current goal is SNo_add_SNo y z Hy2 Hz2.
We prove the intermediate claim Ldry: diadic_rational_p y.
Apply IH (SNoLev y) to the current goal.
We will prove SNoLev y ∈ n.
rewrite the current goal using Hxn (from right to left).
We will prove SNoLev y ∈ SNoLev x.
An exact proof term for the current goal is Hy1b.
We will prove SNo y.
An exact proof term for the current goal is Hy2.
We will prove SNoLev y = SNoLev y.
Use reflexivity.
We prove the intermediate claim Ldrz: diadic_rational_p z.
Apply IH (SNoLev z) to the current goal.
We will prove SNoLev z ∈ n.
rewrite the current goal using Hxn (from right to left).
We will prove SNoLev z ∈ SNoLev x.
An exact proof term for the current goal is Hz1b.
We will prove SNo z.
An exact proof term for the current goal is Hz2.
We will prove SNoLev z = SNoLev z.
Use reflexivity.
Apply SNoLt_trichotomy_or_impred (x + x) (y + z) Lxx Lyz to the current goal.
rewrite the current goal using add_SNo_com y z Hy2 Hz2 (from left to right).
Assume H1: x + x < z + y.
Apply double_SNo_min_1 x z Hx Hz y Hy2 Hy1c H1 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoL y.
Assume H2: z + w = x + x.
Apply SNoL_E y Hy2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Ldrw: diadic_rational_p w.
Apply IH (SNoLev w) to the current goal.
We will prove SNoLev w ∈ n.
Apply ordinal_TransSet n (nat_p_ordinal n Hn) (SNoLev y) to the current goal.
We will prove SNoLev y ∈ n.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hy1b.
We will prove SNoLev w ∈ SNoLev y.
An exact proof term for the current goal is Hw2.
We will prove SNo w.
An exact proof term for the current goal is Hw1.
We will prove SNoLev w = SNoLev w.
Use reflexivity.
We prove the intermediate claim Lxe: x = eps_ 1 * (z + w).
Apply double_eps_1 x z w Hx Hz2 Hw1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (z + w).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p z.
An exact proof term for the current goal is Ldrz.
We will prove diadic_rational_p w.
An exact proof term for the current goal is Ldrw.
Assume H1: x + x = y + z.
We prove the intermediate claim Lxe: x = eps_ 1 * (y + z).
An exact proof term for the current goal is double_eps_1 x y z Hx Hy2 Hz2 H1.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (y + z).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p y.
An exact proof term for the current goal is Ldry.
We will prove diadic_rational_p z.
An exact proof term for the current goal is Ldrz.
Assume H1: y + z < x + x.
Apply double_SNo_max_1 x y Hx Hy z Hz2 Hz1c H1 to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ SNoR z.
Assume H2: y + w = x + x.
Apply SNoR_E z Hz2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
We prove the intermediate claim Ldrw: diadic_rational_p w.
Apply IH (SNoLev w) to the current goal.
We will prove SNoLev w ∈ n.
Apply ordinal_TransSet n (nat_p_ordinal n Hn) (SNoLev z) to the current goal.
We will prove SNoLev z ∈ n.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hz1b.
We will prove SNoLev w ∈ SNoLev z.
An exact proof term for the current goal is Hw2.
We will prove SNo w.
An exact proof term for the current goal is Hw1.
We will prove SNoLev w = SNoLev w.
Use reflexivity.
We prove the intermediate claim Lxe: x = eps_ 1 * (y + w).
Apply double_eps_1 x y w Hx Hy2 Hw1 to the current goal.
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
We will prove diadic_rational_p x.
rewrite the current goal using Lxe (from left to right).
Apply mul_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p (eps_ 1).
An exact proof term for the current goal is eps_diadic_rational_p 1 (nat_p_omega 1 nat_1).
We will prove diadic_rational_p (y + w).
Apply add_SNo_diadic_rational_p to the current goal.
We will prove diadic_rational_p y.
An exact proof term for the current goal is Ldry.
We will prove diadic_rational_p w.
An exact proof term for the current goal is Ldrw.
∎