Let n be given.
Assume Hn.
Let x be given.
Apply dneg to the current goal.
We prove the intermediate
claim LxSo:
x ∈ SNoS_ ω.
rewrite the current goal using Hxn (from left to right).
An
exact proof term for the current goal is
nat_p_omega n Hn.
An exact proof term for the current goal is Hx.
We prove the intermediate
claim L1a:
ordinal (- x).
Let w be given.
rewrite the current goal using
minus_SNo_Lev x Hx (from left to right).
Assume Hw1 Hw2 Hw3 Hw4.
An exact proof term for the current goal is H2.
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 ??.
Apply EmptyE (- w) to the current goal.
rewrite the current goal using H1 (from right to left).
rewrite the current goal using
minus_SNo_Lev w ?? (from left to right).
An exact proof term for the current goal is ??.
We prove the intermediate
claim L1b:
- x = n.
rewrite the current goal using Hxn (from right to left).
Use symmetry.
rewrite the current goal using
minus_SNo_Lev x ?? (from right to left).
Apply HC to the current goal.
rewrite the current goal using L1b (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.
We prove the intermediate
claim L2a:
ordinal x.
Let w be given.
Assume Hw1 Hw2 Hw3 Hw4.
An exact proof term for the current goal is H2.
rewrite the current goal using H2 (from right to left) at position 1.
An exact proof term for the current goal is ??.
Apply EmptyE w to the current goal.
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).
Use symmetry.
Apply HC to the current goal.
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.
Apply Hy to the current goal.
Assume H.
Apply H to the current goal.
Apply SNoL_E x Hx y Hy1 to the current goal.
Assume _ Hy1b Hy1c.
Apply L2 to the current goal.
Let z be given.
Apply Hz to the current goal.
Assume H.
Apply H to the current goal.
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.
Apply IH (SNoLev y) to the current goal.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hy1b.
An exact proof term for the current goal is Hy2.
Apply IH (SNoLev z) to the current goal.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hz1b.
An exact proof term for the current goal is Hz2.
rewrite the current goal using
add_SNo_com y z Hy2 Hz2 (from left to right).
Let w be given.
Assume H.
Apply H to the current goal.
Apply SNoL_E y Hy2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply IH (SNoLev w) to the current goal.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hy1b.
An exact proof term for the current goal is Hw2.
An exact proof term for the current goal is Hw1.
We prove the intermediate
claim Lxe:
x = eps_ 1 * (z + w).
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
rewrite the current goal using Lxe (from left to right).
An exact proof term for the current goal is Ldrz.
An exact proof term for the current goal is Ldrw.
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.
rewrite the current goal using Lxe (from left to right).
An exact proof term for the current goal is Ldry.
An exact proof term for the current goal is Ldrz.
Let w be given.
Assume H.
Apply H to the current goal.
Apply SNoR_E z Hz2 w Hw to the current goal.
Assume Hw1 Hw2 Hw3.
Apply IH (SNoLev w) to the current goal.
rewrite the current goal using Hxn (from right to left).
An exact proof term for the current goal is Hz1b.
An exact proof term for the current goal is Hw2.
An exact proof term for the current goal is Hw1.
We prove the intermediate
claim Lxe:
x = eps_ 1 * (y + w).
Use symmetry.
An exact proof term for the current goal is H2.
Apply HC to the current goal.
rewrite the current goal using Lxe (from left to right).
An exact proof term for the current goal is Ldry.
An exact proof term for the current goal is Ldrw.
∎