DEFINITION lt_le_minus()
TYPE =
       ∀x:nat.∀y:nat.(lt x y)→(le x (minus y (S O)))
BODY =
        assume x: nat
        assume y: nat
        suppose H: lt x y
          (h1) 
             consider H
             we proved lt x y
le (plus (S O) x) y
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus x (S O)) (plus (S O) x)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved le (plus x (S O)) y
          by (le_minus . . . previous)
          we proved le x (minus y (S O))
       we proved ∀x:nat.∀y:nat.(lt x y)→(le x (minus y (S O)))