DEFINITION le_S_minus()
TYPE =
       ∀d:nat.∀h:nat.∀n:nat.(le (plus d h) n)→(le d (S (minus n h)))
BODY =
Show proof