DEFINITION minus_Sn_m()
TYPE =
       ∀n:nat
         .∀m:nat.(le m n)→(eq nat (S (minus n m)) (minus (S n) m))
BODY =
        assume n: nat
        assume m: nat
        suppose Le: le m n
          (h1) 
             assume p: nat
                by (minus_n_O .)
                we proved eq nat p (minus p O)
                by (sym_eq . . . previous)
                we proved eq nat (minus p O) p
                by (f_equal . . . . . previous)
                we proved eq nat (S (minus p O)) (S p)
                that is equivalent to eq nat (S (minus p O)) (minus (S p) O)
∀p:nat.(eq nat (S (minus p O)) (minus (S p) O))
          end of h1
          (h2) 
              assume p: nat
              assume q: nat
              suppose : le p q
                we must prove 
                      eq nat (S (minus q p)) (minus (S q) p)
                        →eq nat (S (minus (S q) (S p))) (minus (S (S q)) (S p))
                or equivalently 
                      (eq
                          nat
                          S (minus q p)
                          <λn1:nat.nat> CASE p OF O⇒S q | S l⇒minus q l)
                        →eq nat (S (minus (S q) (S p))) (minus (S (S q)) (S p))
                suppose H0: 
                   eq
                     nat
                     S (minus q p)
                     <λn1:nat.nat> CASE p OF O⇒S q | S l⇒minus q l
                   consider H0
                   we proved 
                      eq
                        nat
                        S (minus q p)
                        <λn1:nat.nat> CASE p OF O⇒S q | S l⇒minus q l
                   that is equivalent to eq nat (S (minus (S q) (S p))) (minus (S (S q)) (S p))
                we proved 
                   (eq
                       nat
                       S (minus q p)
                       <λn1:nat.nat> CASE p OF O⇒S q | S l⇒minus q l)
                     →eq nat (S (minus (S q) (S p))) (minus (S (S q)) (S p))
                that is equivalent to 
                   eq nat (S (minus q p)) (minus (S q) p)
                     →eq nat (S (minus (S q) (S p))) (minus (S (S q)) (S p))

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