DEFINITION le_minus()
TYPE =
       ∀x:nat.∀z:nat.∀y:nat.(le (plus x y) z)→(le x (minus z y))
BODY =
        assume x: nat
        assume z: nat
        assume y: nat
        suppose H: le (plus x y) z
          by (minus_plus_r . .)
          we proved eq nat (minus (plus x y) y) x
          we proceed by induction on the previous result to prove le x (minus z y)
             case refl_equal : ⇒
                the thesis becomes le (minus (plus x y) y) (minus z y)
                   by (le_plus_r . .)
                   we proved le y (plus x y)
                   by (le_minus_minus . . previous . H)
le (minus (plus x y) y) (minus z y)
          we proved le x (minus z y)
       we proved ∀x:nat.∀z:nat.∀y:nat.(le (plus x y) z)→(le x (minus z y))