| pf |
|---|
Let x0 of type ι be given.
Apply nat_ind with λ x1 . x0 ⊆ x1 ⟶ mul_nat x0 x0 ⊆ mul_nat x1 x1 leaving 2 subgoals.
Assume H1: x0 ⊆ 0.
Apply Empty_Subq_eq with x0, λ x1 x2 . mul_nat x2 x2 ⊆ mul_nat 0 0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying Subq_ref with mul_nat 0 0. Let x1 of type ι be given.
Apply ordinal_In_Or_Subq with x1, x0, mul_nat x0 x0 ⊆ mul_nat (ordsucc x1) (ordsucc x1) leaving 4 subgoals.
Apply nat_p_ordinal with x1.
The subproof is completed by applying H1.
Apply nat_p_ordinal with x0.
The subproof is completed by applying H0.
Assume H4: x1 ∈ x0.
Apply set_ext with x0, ordsucc x1 leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Apply ordsuccE with x1, x2, x2 ∈ x0 leaving 3 subgoals.
The subproof is completed by applying H5.
Assume H6: x2 ∈ x1.
Apply nat_trans with x0, x1, x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Assume H6: x2 = x1.
Apply H6 with λ x3 x4 . x4 ∈ x0.
The subproof is completed by applying H4.
Apply L5 with λ x2 x3 . mul_nat x0 x0 ⊆ mul_nat x2 x2.
The subproof is completed by applying Subq_ref with mul_nat x0 x0. Assume H4: x0 ⊆ x1.
Apply H2.
The subproof is completed by applying H4.
Apply mul_nat_SR with ordsucc x1, x1, λ x2 x3 . mul_nat x0 x0 ⊆ x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply mul_nat_SL with x1, x1, λ x2 x3 . mul_nat x0 x0 ⊆ add_nat (ordsucc x1) x3 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Apply Subq_tra with mul_nat x0 x0, mul_nat x1 x1, add_nat (ordsucc x1) (add_nat (mul_nat x1 x1) x1) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply add_nat_p with mul_nat x1 x1, x1 leaving 2 subgoals.
Apply mul_nat_p with x1, x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Apply add_nat_SL with x1, add_nat (mul_nat x1 x1) x1, λ x2 x3 . mul_nat x1 x1 ⊆ x3 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L6.
Apply Subq_tra with mul_nat x1 x1, add_nat x1 (add_nat (mul_nat x1 x1) x1), ordsucc (add_nat x1 (add_nat (mul_nat x1 x1) x1)) leaving 2 subgoals.
Apply Subq_tra with mul_nat x1 x1, add_nat (mul_nat x1 x1) x1, add_nat x1 (add_nat (mul_nat x1 x1) x1) leaving 2 subgoals.
Apply add_nat_Subq_L with mul_nat x1 x1, x1 leaving 2 subgoals.
Apply mul_nat_p with x1, x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Apply add_nat_com with x1, add_nat (mul_nat x1 x1) x1, λ x2 x3 . add_nat (mul_nat x1 x1) x1 ⊆ x3 leaving 3 subgoals.
The subproof is completed by applying H1.
Apply add_nat_p with mul_nat x1 x1, x1 leaving 2 subgoals.
Apply mul_nat_p with x1, x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Apply add_nat_Subq_L with add_nat (mul_nat x1 x1) x1, x1 leaving 2 subgoals.
Apply add_nat_p with mul_nat x1 x1, x1 leaving 2 subgoals.
Apply mul_nat_p with x1, x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
■ |
|