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