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