DEFINITION le_gen_S()
TYPE =
       ∀m:nat
         .∀x:nat.(le (S m) x)→(ex2 nat λn:nat.eq nat x (S n) λn:nat.le m n)
BODY =
Show proof