DEFINITION le_minus_minus()
TYPE =
       ∀x:nat
         .∀y:nat
           .(le x y)→∀z:nat.(le y z)→(le (minus y x) (minus z x))
BODY =
        assume x: nat
        assume y: nat
        suppose H: le x y
        assume z: nat
        suppose H0: le y z
          (h1) 
             by (le_trans . . . H H0)
             we proved le x z
             by (le_plus_minus_r . . previous)
             we proved eq nat (plus x (minus z x)) z
             by (eq_ind_r . . . H0 . previous)
le y (plus x (minus z x))
          end of h1
          (h2) 
             by (le_plus_minus_r . . H)
eq nat (plus x (minus y x)) y
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved le (plus x (minus y x)) (plus x (minus z x))
          by (simpl_le_plus_l . . . previous)
          we proved le (minus y x) (minus z x)
       we proved 
          ∀x:nat
            .∀y:nat
              .(le x y)→∀z:nat.(le y z)→(le (minus y x) (minus z x))