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