Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_06a4ec1d06df31c2c8c53ecdf2780bb9f187c1468b28741ccdfd338035b0de7f with
mul_CSNo x0 x1,
mul_CSNo (minus_CSNo x0) x1,
minus_CSNo (mul_CSNo x0 x1) leaving 4 subgoals.
The subproof is completed by applying L2.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
minus_CSNo x0,
x1 leaving 2 subgoals.
Apply CSNo_minus_CSNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply CSNo_minus_CSNo with
mul_CSNo x0 x1.
The subproof is completed by applying L2.
Apply add_CSNo_minus_CSNo_rinv with
mul_CSNo x0 x1,
λ x2 x3 . add_CSNo (mul_CSNo x0 x1) (mul_CSNo (minus_CSNo x0) x1) = x3 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply unknownprop_8e63a35ced1c21572795aec3dca7302bd96cc84c909ac1e26265b0a88a4ddf7f with
x0,
minus_CSNo x0,
x1,
λ x2 x3 . x2 = 0 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply CSNo_minus_CSNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply add_CSNo_minus_CSNo_rinv with
x0,
λ x2 x3 . mul_CSNo x3 x1 = 0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_2a5a876481120fa10aa7abde74e1fdc7c8706213e1f397e994cc370e961fee2d with
x1.
The subproof is completed by applying H1.