Proofgold Proof

pf
Apply minus_SNo_Lt_contra1 with 0, 1 leaving 3 subgoals. The subproof is completed by applying SNo_0. The subproof is completed by applying SNo_1. Apply minus_SNo_0 with λ x0 x1 . SNoLt x1 1. The subproof is completed by applying SNoLt_0_1. ■