DEFINITION minus_Sn_m()
TYPE =
       ∀n:nat
         .∀m:nat.(le m n)→(eq nat (S (minus n m)) (minus (S n) m))
BODY =
Show proof