| pf |
|---|
Apply nat_ind with λ x0 . ∀ x1 . x1 ∈ ordsucc (ordsucc x0) ⟶ ordsucc (mul_nat x1 x1) ∈ mul_nat (ordsucc (ordsucc x0)) (ordsucc (ordsucc x0)) leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: x0 ∈ 2.
Apply mul_nat_SR with 2, 1, λ x1 x2 . ordsucc (mul_nat x0 x0) ∈ x2 leaving 2 subgoals.
The subproof is completed by applying nat_1.
Apply mul_nat_1R with 2, λ x1 x2 . ordsucc (mul_nat x0 x0) ∈ add_nat 2 x2.
Apply add_nat_SR with 2, 1, λ x1 x2 . ordsucc (mul_nat x0 x0) ∈ x2 leaving 2 subgoals.
The subproof is completed by applying nat_1.
Apply add_nat_SR with 2, 0, λ x1 x2 . ordsucc (mul_nat x0 x0) ∈ ordsucc x2 leaving 2 subgoals.
The subproof is completed by applying nat_0.
Apply add_nat_0R with 2, λ x1 x2 . ordsucc (mul_nat x0 x0) ∈ ordsucc (ordsucc x2).
Apply cases_2 with x0, λ x1 . ordsucc (mul_nat x1 x1) ∈ 4 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_0R with 0, λ x1 x2 . ordsucc x2 ∈ 4.
The subproof is completed by applying In_1_4.
Apply mul_nat_1R with 1, λ x1 x2 . ordsucc x2 ∈ 4.
The subproof is completed by applying In_2_4.
Let x0 of type ι be given.
Let x1 of type ι be given.
■ |
|