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 SNoLt_irref with
0.
Apply SNoLeLt_tra with
0,
add_SNo x2 x3,
0 leaving 5 subgoals.
The subproof is completed by applying SNo_0.
Apply SNo_add_SNo with
x2,
x3 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying SNo_0.
Apply add_SNo_com with
x0,
minus_SNo x1,
λ x4 x5 . SNoLe (add_SNo (add_SNo x1 (minus_SNo x0)) x5) (add_SNo x2 x3) ⟶ SNoLe 0 (add_SNo x2 x3) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
x1.
The subproof is completed by applying H1.
Apply add_SNo_com_4_inner_mid with
x1,
minus_SNo x0,
minus_SNo x1,
x0,
λ x4 x5 . SNoLe x5 (add_SNo x2 x3) ⟶ SNoLe 0 (add_SNo x2 x3) leaving 5 subgoals.
The subproof is completed by applying H1.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply add_SNo_minus_SNo_rinv with
x1,
λ x4 x5 . SNoLe (add_SNo x5 (add_SNo (minus_SNo x0) x0)) (add_SNo x2 x3) ⟶ SNoLe 0 (add_SNo x2 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply add_SNo_minus_SNo_linv with
x0,
λ x4 x5 . SNoLe (add_SNo 0 x5) (add_SNo x2 x3) ⟶ SNoLe 0 (add_SNo x2 x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_SNo_0L with
0,
λ x4 x5 . SNoLe x5 (add_SNo x2 x3) ⟶ SNoLe 0 (add_SNo x2 x3) leaving 2 subgoals.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H7.
Apply L7.
Apply add_SNo_Le3 with
add_SNo x1 (minus_SNo x0),
add_SNo x0 (minus_SNo x1),
x2,
x3 leaving 6 subgoals.
Apply SNo_add_SNo with
x1,
minus_SNo x0 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply SNo_minus_SNo with
x0.
The subproof is completed by applying H0.
Apply SNo_add_SNo with
x0,
minus_SNo x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNo_minus_SNo with
x1.
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 H6.
The subproof is completed by applying H4.