DEFINITION le_plus_minus()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(eq nat m (plus n (minus m n)))
BODY =
        assume n: nat
        assume m: nat
        suppose Le: le n m
          (h1) 
             assume p: nat
                by (minus_n_O .)
                we proved eq nat p (minus p O)
                that is equivalent to eq nat p (plus O (minus p O))
∀p:nat.(eq nat p (plus O (minus p O)))
          end of h1
          (h2) 
              assume p: nat
              assume q: nat
              suppose : le p q
              suppose H0: eq nat q (plus p (minus q p))
                by (f_equal . . . . . H0)
                we proved eq nat (S q) (S (plus p (minus q p)))
                that is equivalent to eq nat (S q) (plus (S p) (minus (S q) (S p)))

                ∀p:nat
                  .∀q:nat
                    .le p q
                      →(eq nat q (plus p (minus q p))
                           →eq nat (S q) (plus (S p) (minus (S q) (S p))))
          end of h2
          by (le_elim_rel . h1 h2 . . Le)
          we proved eq nat m (plus n (minus m n))
       we proved ∀n:nat.∀m:nat.(le n m)→(eq nat m (plus n (minus m n)))