Let x0 of type ι be given.
Apply H0 with
diadic_rational_alt1_p (minus_SNo x0).
Let x1 of type ι be given.
Apply H1 with
diadic_rational_alt1_p (minus_SNo x0).
Assume H2:
x1 ∈ omega.
Apply H3 with
diadic_rational_alt1_p (minus_SNo x0).
Let x2 of type ι be given.
Apply H4 with
diadic_rational_alt1_p (minus_SNo x0).
Let x3 of type ο be given.
Apply H7 with
x1.
Apply andI with
x1 ∈ omega,
∃ x4 . and (x4 ∈ int_alt1) (minus_SNo x0 = mul_SNo (eps_ x1) x4) leaving 2 subgoals.
The subproof is completed by applying H2.
Let x4 of type ο be given.
Apply H8 with
minus_SNo x2.
Apply andI with
minus_SNo x2 ∈ int_alt1,
minus_SNo x0 = mul_SNo (eps_ x1) (minus_SNo x2) leaving 2 subgoals.
Apply unknownprop_66d7a7b7f8768657be1ea35e52473cc5e1846e635153a280e3783a8275062773 with
x2.
The subproof is completed by applying H5.
Apply mul_SNo_minus_distrR with
eps_ x1,
x2,
λ x5 x6 . minus_SNo x0 = x6 leaving 3 subgoals.
Apply SNo_eps_ with
x1.
The subproof is completed by applying H2.
Apply unknownprop_21e78e4ab287a999eff678dc5fdcb4fe6daaa47d39850e6dedc392cb88159c27 with
x2.
The subproof is completed by applying H5.
Claim L9:
∀ x6 : ι → ο . x6 y5 ⟶ x6 (minus_SNo x0)
Let x6 of type ι → ο be given.
The subproof is completed by applying H6 with
λ x7 x8 . (λ x9 . x6) (minus_SNo x7) (minus_SNo x8).
Let x6 of type ι → ι → ο be given.
Apply L9 with
λ x7 . x6 x7 y5 ⟶ x6 y5 x7.
Assume H10: x6 y5 y5.
The subproof is completed by applying H10.