Let x be given.
Assume Hx Hxnonneg H1 H1R.
rewrite the current goal using
SNoCut_0_0 (from right to left) at position 1.
Set L to be the term
⋃k ∈ ωL_ k.
Set R to be the term
⋃k ∈ ωR_ k.
An
exact proof term for the current goal is
SNoCutP_0_0.
An exact proof term for the current goal is H1.
Let w be given.
An
exact proof term for the current goal is
EmptyE w Hw.
Let z be given.
rewrite the current goal using
SNoCut_0_0 (from left to right).
Apply H1R z Hz to the current goal.
An exact proof term for the current goal is H6.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hz3.
An exact proof term for the current goal is Hxnonneg.
∎