Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_b9f761a9aaf971afc2c321abccc5415a4ba796124b1aaa309d3f974fda1d3d26 with
2 leaving 2 subgoals.
The subproof is completed by applying unknownprop_3729fc97c8b5f21188ac361733273781ed00775a9662ac2f2237f0346be243d1.
Apply int_SNo with
x1.
The subproof is completed by applying H1.
Apply SNo_mul_SNo with
2,
x1 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying L3.
Apply SNo_mul_SNo with
2,
x0 leaving 2 subgoals.
The subproof is completed by applying SNo_2.
Apply int_SNo with
x0.
The subproof is completed by applying H0.
Apply mul_SNo_distrL with
2,
x0,
minus_SNo x1,
λ x2 x3 . x3 = 1,
λ x2 x3 . divides_int 2 x2 leaving 5 subgoals.
The subproof is completed by applying SNo_2.
Apply int_SNo with
x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
x1.
The subproof is completed by applying L3.
Apply mul_SNo_minus_distrR with
2,
x1,
λ x2 x3 . add_SNo (mul_SNo 2 x0) x3 = 1 leaving 3 subgoals.
The subproof is completed by applying SNo_2.
The subproof is completed by applying L3.
Apply add_SNo_cancel_L with
mul_SNo 2 x1,
add_SNo (mul_SNo 2 x0) (minus_SNo (mul_SNo 2 x1)),
1 leaving 4 subgoals.
The subproof is completed by applying L4.
Apply SNo_add_SNo with
mul_SNo 2 x0,
minus_SNo (mul_SNo 2 x1) leaving 2 subgoals.
The subproof is completed by applying L5.
Apply SNo_minus_SNo with
mul_SNo 2 x1.
The subproof is completed by applying L4.
The subproof is completed by applying SNo_1.
Apply H2 with
λ x2 x3 . add_SNo (mul_SNo 2 x1) (add_SNo (mul_SNo 2 x0) (minus_SNo (mul_SNo 2 x1))) = x2.
Apply add_SNo_rotate_3_1 with
mul_SNo 2 x1,
mul_SNo 2 x0,
minus_SNo (mul_SNo 2 x1),
λ x2 x3 . x3 = mul_SNo 2 x0 leaving 4 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply SNo_minus_SNo with
mul_SNo 2 x1.
The subproof is completed by applying L4.
Apply add_SNo_minus_L2 with
mul_SNo 2 x1,
mul_SNo 2 x0 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
Apply divides_int_mul_SNo_L with
2,
2,
add_SNo x0 (minus_SNo x1) leaving 2 subgoals.
Apply int_add_SNo with
x0,
minus_SNo x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply int_minus_SNo with
x1.
The subproof is completed by applying H1.
Apply divides_int_ref with
2.
Apply Subq_omega_int with
2.
Apply nat_p_omega with
2.
The subproof is completed by applying nat_2.