Apply unknownprop_b35032c81ea06ad673f8a0490d5be4e7b984453ec9378fed4adde429c2b88d75 with
λ x0 . ∀ x1 . nat_p x1 ⟶ mul_nat x1 x0 = x1 ⟶ (x1 = 0 ⟶ ∀ x2 : ο . x2) ⟶ x0 = 1 leaving 3 subgoals.
Let x0 of type ι be given.
Apply mul_nat_0R with
x0,
λ x1 x2 . x2 = x0 ⟶ (x0 = 0 ⟶ ∀ x3 : ο . x3) ⟶ 0 = 1.
Assume H1: 0 = x0.
Assume H2: x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply FalseE with
0 = 1.
Apply H2.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H1 with λ x2 x3 . x1 x3 x2.
Let x0 of type ι be given.
Assume H2: x0 = 0 ⟶ ∀ x1 : ο . x1.
Let x1 of type ι → ι → ο be given.
Assume H3: x1 1 1.
The subproof is completed by applying H3.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply mul_nat_SR with
x1,
ordsucc x0,
λ x2 x3 . x3 = x1 ⟶ (x1 = 0 ⟶ ∀ x4 : ο . x4) ⟶ ordsucc (ordsucc x0) = 1 leaving 2 subgoals.
Apply nat_ordsucc with
x0.
The subproof is completed by applying H0.
Apply mul_nat_SR with
x1,
x0,
λ x2 x3 . add_nat x1 x3 = x1 ⟶ (x1 = 0 ⟶ ∀ x4 : ο . x4) ⟶ ordsucc (ordsucc x0) = 1 leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H3: x1 = 0 ⟶ ∀ x2 : ο . x2.
Apply FalseE with
ordsucc (ordsucc x0) = 1.
Apply add_nat_com with
add_nat x1 (mul_nat x1 x0),
x1,
λ x2 x3 . x3 = x1 leaving 3 subgoals.
Apply add_nat_p with
x1,
mul_nat x1 x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply mul_nat_p with
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_986be96dc315caaba0467a55e70dc4d242dfd7d790ce55390e38a5d935288972 with
add_nat x1 (mul_nat x1 x0),
x1 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
Apply unknownprop_6983d26e930e4f29d8bfcdef860e7bdda90fb8cfa66e4db9cfa2a0c77f2e095e with
x1,
mul_nat x1 x0,
False leaving 3 subgoals.
Apply mul_nat_p with
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying L5.
Assume H6: x1 = 0.
Apply FalseE with
mul_nat x1 x0 = 0 ⟶ False.
Apply H3.
The subproof is completed by applying H6.