Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: nat_p x0.
Let x1 of type ι be given.
Assume H1: x1setminus omega 1.
Apply unknownprop_e18849ea271b9fad1d1f55210e57a4e42a5b850b4f5bda4268b35baef08a0fd5 with x1, x0mul_nat x0 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x2 of type ι be given.
Assume H2: x2omega.
Assume H3: x1 = ordsucc x2.
Apply H3 with λ x3 x4 . x0mul_nat x0 x4.
Apply mul_nat_SR with x0, x2, λ x3 x4 . x0x4 leaving 2 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H2.
Apply add_nat_Subq_L with x0, mul_nat x0 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply mul_nat_p with x0, x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply omega_nat_p with x2.
The subproof is completed by applying H2.