DEFINITION simpl_lt_plus_l()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(lt (plus p n) (plus p m))→(lt n m)
BODY =
Show proof