Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: nat_p x0.
Assume H1: nat_p x1.
Assume H2: 0x0.
Assume H3: 1x1.
Claim L4: ordinal x0
Apply nat_p_ordinal with x0.
The subproof is completed by applying H0.
Claim L5: ordinal x1
Apply nat_p_ordinal with x1.
The subproof is completed by applying H1.
Claim L6: SNo x0
Apply ordinal_SNo with x0.
The subproof is completed by applying L4.
Claim L7: SNo x1
Apply ordinal_SNo with x1.
The subproof is completed by applying L5.
Claim L8: SNoLt 0 x0
Apply ordinal_In_SNoLt with x0, 0 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
Claim L9: SNoLt 1 x1
Apply ordinal_In_SNoLt with x1, 1 leaving 2 subgoals.
The subproof is completed by applying L5.
The subproof is completed by applying H3.
Apply ordinal_SNoLt_In with x0, mul_nat x0 x1 leaving 3 subgoals.
The subproof is completed by applying L4.
Apply nat_p_ordinal with mul_nat x0 x1.
Apply mul_nat_p with x0, x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply mul_nat_mul_SNo with x0, x1, λ x2 x3 . SNoLt x0 x3 leaving 3 subgoals.
Apply nat_p_omega with x0.
The subproof is completed by applying H0.
Apply nat_p_omega with x1.
The subproof is completed by applying H1.
Apply add_SNo_0L with x0, λ x2 x3 . SNoLt x2 (mul_SNo x0 x1) leaving 2 subgoals.
The subproof is completed by applying L6.
Apply add_SNo_minus_Lt2 with mul_SNo x0 x1, x0, 0 leaving 4 subgoals.
Apply SNo_mul_SNo with x0, x1 leaving 2 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
The subproof is completed by applying L6.
The subproof is completed by applying SNo_0.
Apply mul_SNo_oneR with x0, λ x2 x3 . SNoLt 0 (add_SNo (mul_SNo x0 x1) (minus_SNo x2)) leaving 2 subgoals.
The subproof is completed by applying L6.
Apply mul_SNo_minus_distrR with x0, 1, λ x2 x3 . SNoLt 0 (add_SNo (mul_SNo x0 x1) x2) leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying SNo_1.
Apply mul_SNo_distrL with x0, x1, minus_SNo 1, λ x2 x3 . SNoLt 0 x2 leaving 4 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L7.
Apply SNo_minus_SNo with 1.
The subproof is completed by applying SNo_1.
Apply mul_SNo_pos_pos with x0, add_SNo x1 (minus_SNo 1) leaving 4 subgoals.
The subproof is completed by applying L6.
Apply SNo_add_SNo with x1, minus_SNo 1 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply SNo_minus_SNo with 1.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L8.
Apply add_SNo_minus_Lt2b with x1, 1, 0 leaving 4 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying SNo_1.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with 1, λ x2 x3 . SNoLt x3 x1 leaving 2 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L9.