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