| pf |
|---|
Apply nat_ind with λ x0 . ∀ x1 . x1 ∈ x0 ⟶ ordsucc (mul_nat x1 x1) ⊆ mul_nat x0 x0 leaving 2 subgoals.
Let x0 of type ι be given.
Assume H0: x0 ∈ 0.
Apply FalseE with ordsucc (mul_nat x0 x0) ⊆ mul_nat 0 0.
Apply EmptyE with x0.
The subproof is completed by applying H0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply nat_ordsucc with x0.
The subproof is completed by applying H0.
Apply mul_nat_SL with x0, ordsucc x0, λ x2 x3 . ordsucc (mul_nat x1 x1) ⊆ x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply ordsuccE with x0, x1, ordsucc (mul_nat x1 x1) ⊆ add_nat (mul_nat x0 (ordsucc x0)) (ordsucc x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Assume H4: x1 ∈ x0.
Apply Subq_tra with ordsucc (mul_nat x1 x1), mul_nat x0 (ordsucc x0), add_nat (mul_nat x0 (ordsucc x0)) (ordsucc x0) leaving 2 subgoals.
Apply mul_nat_SR with x0, x0, λ x2 x3 . ordsucc (mul_nat x1 x1) ⊆ x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply Subq_tra with ordsucc (mul_nat x1 x1), mul_nat x0 x0, add_nat x0 (mul_nat x0 x0) leaving 2 subgoals.
Apply H1 with x1.
The subproof is completed by applying H4.
Apply add_nat_com with x0, mul_nat x0 x0, λ x2 x3 . mul_nat x0 x0 ⊆ x3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_p with x0, x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply add_nat_Subq_L with mul_nat x0 x0, x0 leaving 2 subgoals.
Apply mul_nat_p with x0, x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply add_nat_Subq_L with mul_nat x0 (ordsucc x0), ordsucc x0 leaving 2 subgoals.
Apply mul_nat_p with x0, ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying L3.
Assume H4: x1 = x0.
Apply H4 with λ x2 x3 . ordsucc (mul_nat x3 x3) ⊆ add_nat (mul_nat x0 (ordsucc x0)) (ordsucc x0).
Apply add_nat_SR with mul_nat x0 (ordsucc x0), x0, λ x2 x3 . ordsucc (mul_nat x0 x0) ⊆ x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_7efa9b0eb4a7672f89f79f79d5dfd89fdd189d47f4be668ddc1bdc4223ecb821 with mul_nat x0 x0, add_nat (mul_nat x0 (ordsucc x0)) x0 leaving 3 subgoals.
Apply nat_p_ordinal with mul_nat x0 x0.
Apply mul_nat_p with x0, x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply nat_p_ordinal with add_nat (mul_nat x0 (ordsucc x0)) x0.
Apply add_nat_p with mul_nat x0 (ordsucc x0), x0 leaving 2 subgoals.
Apply mul_nat_p with x0, ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying H0.
Apply Subq_tra with mul_nat x0 x0, mul_nat x0 (ordsucc x0), add_nat (mul_nat x0 (ordsucc x0)) x0 leaving 2 subgoals.
Apply mul_nat_SR with x0, x0, λ x2 x3 . mul_nat x0 x0 ⊆ x3 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_nat_com with x0, mul_nat x0 x0, λ x2 x3 . mul_nat x0 x0 ⊆ x3 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_p with x0, x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply add_nat_Subq_L with mul_nat x0 x0, x0 leaving 2 subgoals.
Apply mul_nat_p with x0, x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
Apply add_nat_Subq_L with mul_nat x0 (ordsucc x0), x0 leaving 2 subgoals.
Apply mul_nat_p with x0, ordsucc x0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
The subproof is completed by applying H0.
■ |
|