Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply SNoLeE with
add_SNo x0 x1,
add_SNo x3 x2,
SNoLe (add_SNo x0 (add_SNo x1 (minus_SNo x2))) x3 leaving 5 subgoals.
Apply SNo_add_SNo with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNo_add_SNo with
x3,
x2 leaving 2 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying H2.
The subproof is completed by applying H4.
Apply SNoLtLe with
add_SNo x0 (add_SNo x1 (minus_SNo x2)),
x3.
Apply add_SNo_minus_Lt1b3 with
x0,
x1,
x2,
x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
Apply unknownprop_f60128c069b21c68fcc57ff600ddce543316da609ce5973425d4e18fa598e297 with
x0,
x1,
x2,
x3,
λ x4 x5 . SNoLe x5 x3 leaving 6 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H5.
The subproof is completed by applying SNoLe_ref with x3.