Proofgold Proof

pf
Apply OSNo_proj1_2 with 0, minus_HSNo Complex_i leaving 2 subgoals. The subproof is completed by applying HSNo_0. Apply HSNo_minus_HSNo with Complex_i. The subproof is completed by applying HSNo_Complex_i. ■