| pf |
|---|
Apply int_SNo_cases with λ x0 . ∀ x1 . x1 ∈ int ⟶ add_SNo x0 x1 ∈ int leaving 2 subgoals.
Let x0 of type ι be given.
Apply int_SNo_cases with λ x1 . add_SNo x0 x1 ∈ int leaving 2 subgoals.
Let x1 of type ι be given.
Apply Subq_omega_int with add_SNo x0 x1.
Apply add_SNo_In_omega with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply add_SNo_com with x0, minus_SNo x1, λ x2 x3 . x3 ∈ int leaving 3 subgoals.
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with x1.
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H1.
Apply int_add_SNo_lem with x1, x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Apply int_SNo_cases with λ x1 . add_SNo (minus_SNo x0) x1 ∈ int leaving 2 subgoals.
Let x1 of type ι be given.
Apply int_add_SNo_lem with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply omega_nat_p with x1.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply minus_add_SNo_distr with x0, x1, λ x2 x3 . x2 ∈ int leaving 3 subgoals.
Apply ordinal_SNo with x0.
Apply nat_p_ordinal with x0.
Apply omega_nat_p with x0.
The subproof is completed by applying H0.
Apply ordinal_SNo with x1.
Apply nat_p_ordinal with x1.
Apply omega_nat_p with x1.
The subproof is completed by applying H1.
Apply int_minus_SNo_omega with add_SNo x0 x1.
Apply add_SNo_In_omega with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
■ |
|