DEFINITION plus_minus()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat n (plus m p))→(eq nat p (minus n m))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
          (h1) 
             assume n0: nat
                we must prove (eq nat n0 (plus O p))→(eq nat p (minus n0 O))
                or equivalently (eq nat n0 p)→(eq nat p (minus n0 O))
                suppose H: eq nat n0 p
                   by (minus_n_O .)
                   we proved eq nat n0 (minus n0 O)
                   we proceed by induction on the previous result to prove eq nat p (minus n0 O)
                      case refl_equal : ⇒
                         the thesis becomes eq nat p n0
                            by (sym_eq . . . H)
eq nat p n0
                   we proved eq nat p (minus n0 O)
                we proved (eq nat n0 p)→(eq nat p (minus n0 O))
                that is equivalent to (eq nat n0 (plus O p))→(eq nat p (minus n0 O))
∀n0:nat.(eq nat n0 (plus O p))→(eq nat p (minus n0 O))
          end of h1
          (h2) 
             assume n0: nat
                we must prove (eq nat O (plus (S n0) p))→(eq nat p (minus O (S n0)))
                or equivalently (eq nat O (S (plus n0 p)))→(eq nat p (minus O (S n0)))
                suppose H: eq nat O (S (plus n0 p))
                   (H0) consider H
                   (H1) 
                      by (O_S .)
not (eq nat O (S (plus n0 p)))
                   end of H1
                   suppose H2: eq nat O (S (plus n0 p))
                      by (H1 H2)
                      we proved False
                   we proved (eq nat O (S (plus n0 p)))→False
                   by (previous H0)
                   we proved False
                   we proceed by induction on the previous result to prove eq nat p O
                   we proved eq nat p O
                   that is equivalent to eq nat p (minus O (S n0))
                we proved (eq nat O (S (plus n0 p)))→(eq nat p (minus O (S n0)))
                that is equivalent to (eq nat O (plus (S n0) p))→(eq nat p (minus O (S n0)))
∀n0:nat.(eq nat O (plus (S n0) p))→(eq nat p (minus O (S n0)))
          end of h2
          (h3) 
              assume n0: nat
              assume m0: nat
              suppose H: (eq nat m0 (plus n0 p))→(eq nat p (minus m0 n0))
                we must prove (eq nat (S m0) (plus (S n0) p))→(eq nat p (minus (S m0) (S n0)))
                or equivalently (eq nat (S m0) (S (plus n0 p)))→(eq nat p (minus (S m0) (S n0)))
                suppose H0: eq nat (S m0) (S (plus n0 p))
                   by (eq_add_S . . H0)
                   we proved eq nat m0 (plus n0 p)
                   by (H previous)
                   we proved eq nat p (minus m0 n0)
                   that is equivalent to eq nat p (minus (S m0) (S n0))
                we proved (eq nat (S m0) (S (plus n0 p)))→(eq nat p (minus (S m0) (S n0)))
                that is equivalent to (eq nat (S m0) (plus (S n0) p))→(eq nat p (minus (S m0) (S n0)))

                ∀n0:nat
                  .∀m0:nat
                    .(eq nat m0 (plus n0 p))→(eq nat p (minus m0 n0))
                      →(eq nat (S m0) (plus (S n0) p))→(eq nat p (minus (S m0) (S n0)))
          end of h3
          by (nat_double_ind . h1 h2 h3 . .)
          we proved (eq nat n (plus m p))→(eq nat p (minus n m))
       we proved ∀n:nat.∀m:nat.∀p:nat.(eq nat n (plus m p))→(eq nat p (minus n m))