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