Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply SNoR_E with
x0,
x1,
SNoLt 1 (mul_SNo x0 x4) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply SNo_mul_SNo with
x0,
x3 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H5.
Apply add_SNo_0L with
mul_SNo x0 x4,
λ x5 x6 . SNoLt 1 x5 leaving 2 subgoals.
Apply SNo_mul_SNo with
x0,
x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
Apply add_SNo_minus_Lt1 with
1,
mul_SNo x0 x4,
0 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
Apply SNo_mul_SNo with
x0,
x4 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H7.
The subproof is completed by applying SNo_0.
Apply H8 with
λ x5 x6 . SNoLt x6 0.
Apply mul_SNo_neg_pos with
add_SNo 1 (minus_SNo (mul_SNo x0 x3)),
mul_SNo (add_SNo x1 (minus_SNo x0)) x2 leaving 4 subgoals.
Apply SNo_add_SNo with
1,
minus_SNo (mul_SNo x0 x3) leaving 2 subgoals.
The subproof is completed by applying SNo_1.
Apply SNo_minus_SNo with
mul_SNo x0 x3.
The subproof is completed by applying L12.
Apply SNo_mul_SNo with
add_SNo x1 (minus_SNo x0),
x2 leaving 2 subgoals.
Apply SNo_add_SNo with
x1,
minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply add_SNo_minus_Lt1b with
1,
mul_SNo x0 x3,
0 leaving 4 subgoals.
The subproof is completed by applying SNo_1.
The subproof is completed by applying L12.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with
mul_SNo x0 x3,
λ x5 x6 . SNoLt 1 x6 leaving 2 subgoals.
The subproof is completed by applying L12.
The subproof is completed by applying H6.
Apply mul_SNo_pos_pos with
add_SNo x1 (minus_SNo x0),
x2 leaving 4 subgoals.
Apply SNo_add_SNo with
x1,
minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying H9.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply add_SNo_minus_Lt2b with
x1,
x0,
0 leaving 4 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Apply add_SNo_0L with
x0,
λ x5 x6 . SNoLt x6 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H11.
Apply SNo_recip_pos_pos with
x1,
x2 leaving 4 subgoals.
The subproof is completed by applying H9.
The subproof is completed by applying H3.
Apply SNoLt_tra with
0,
x0,
x1 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H0.
The subproof is completed by applying H9.
The subproof is completed by applying H1.
The subproof is completed by applying H11.
The subproof is completed by applying H4.