Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_78927d114a9e016b6fa814cd3cb647b02601a2956c15aa990b929c9491fbf104 with
x0,
minus_CSNo x1,
λ x2 x3 . x3 = mul_CSNo x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply CSNo_minus_CSNo with
x1.
The subproof is completed by applying H1.
Apply unknownprop_2f3abf0dc8f8a8be1aa9d298d1fecff1a496796abe903d77feb6f0e5457defc1 with
x0,
x1,
λ x2 x3 . minus_CSNo x3 = mul_CSNo x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_cb3c73e6397c4921a333f973bae46a7e59f433123dea81f3a2d0adee769cf93f with
mul_CSNo x0 x1.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.