Added inductive version of ∸-N.
Simplified S∸S proof.
Added inductive version of S∸S.