DEFINITION lt_le_minus()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(le x (minus y (S O)))
BODY =
Show proof