Let x0 of type ι be given.
Apply CSNo_minus_CSNo with
x0.
The subproof is completed by applying H0.
Apply unknownprop_06a4ec1d06df31c2c8c53ecdf2780bb9f187c1468b28741ccdfd338035b0de7f with
minus_CSNo x0,
minus_CSNo (minus_CSNo x0),
x0 leaving 4 subgoals.
The subproof is completed by applying L1.
Apply CSNo_minus_CSNo with
minus_CSNo x0.
The subproof is completed by applying L1.
The subproof is completed by applying H0.
Apply add_CSNo_minus_CSNo_linv with
x0,
λ x1 x2 . add_CSNo (minus_CSNo x0) (minus_CSNo (minus_CSNo x0)) = x2 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_CSNo_minus_CSNo_rinv with
minus_CSNo x0.
The subproof is completed by applying L1.