Let x0 of type ι be given.
Let x1 of type ι be given.
Apply nat_inv with
x1,
mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0) leaving 3 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H1.
Assume H2: x1 = 0.
Apply orIR with
x0 = 0,
x1 = 0.
The subproof is completed by applying H2.
Apply H2 with
mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0).
Let x2 of type ι be given.
Apply H3 with
mul_nat x0 x1 = 0 ⟶ or (x0 = 0) (x1 = 0).
Apply H5 with
λ x3 x4 . mul_nat x0 x4 = 0 ⟶ or (x0 = 0) (x4 = 0).
Apply mul_nat_SR with
x0,
x2,
λ x3 x4 . x4 = 0 ⟶ or (x0 = 0) (ordsucc x2 = 0) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply add_nat_0_inv with
x0,
mul_nat x0 x2,
or (x0 = 0) (ordsucc x2 = 0) leaving 4 subgoals.
The subproof is completed by applying H0.
Apply nat_p_omega with
mul_nat x0 x2.
Apply mul_nat_p with
x0,
x2 leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H6.
Assume H7: x0 = 0.
Apply orIL with
x0 = 0,
ordsucc x2 = 0.
The subproof is completed by applying H7.