Apply CD_minus_add with
Sing 2,
SNo,
minus_SNo,
add_SNo leaving 4 subgoals.
The subproof is completed by applying complex_tag_fresh.
The subproof is completed by applying SNo_minus_SNo.
The subproof is completed by applying SNo_add_SNo.
The subproof is completed by applying minus_add_SNo_distr.