DEFINITION le_S_minus()
TYPE =
       ∀d:nat.∀h:nat.∀n:nat.(le (plus d h) n)→(le d (S (minus n h)))
BODY =
        assume d: nat
        assume h: nat
        assume n: nat
        suppose H: le (plus d h) n
          (H0) 
             by (le_plus_l . .)
             we proved le d (plus d h)
             by (le_trans . . . previous H)
le d n
          end of H0
          by (le_minus . . . H)
          we proved le d (minus n h)
          by (le_S . . previous)
          we proved le d (S (minus n h))
       we proved ∀d:nat.∀h:nat.∀n:nat.(le (plus d h) n)→(le d (S (minus n h)))