DEFINITION le_antisym()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(le m n)→(eq nat n m)
BODY =
        assume n: nat
        assume m: nat
        suppose h: le n m
          we proceed by induction on h to prove (le m n)→(eq nat n m)
             case le_n : ⇒
                the thesis becomes (le n n)→(eq nat n n)
                   suppose : le n n
                      by (refl_equal . .)
                      we proved eq nat n n
(le n n)→(eq nat n n)
             case le_S : m0:nat H:le n m0 ⇒
                the thesis becomes ∀H1:(le (S m0) n).(eq nat n (S m0))
                () by induction hypothesis we know (le m0 n)→(eq nat n m0)
                   suppose H1: le (S m0) n
                      (H2) 
                         by (le_trans . . . H1 H)
le (S m0) m0
                      end of H2
                      (H3) 
                         by (le_Sn_n .)
not (le (S m0) m0)
                      end of H3
                      suppose H4: le (S m0) m0
                         by (H3 H4)
                         we proved False
                      we proved (le (S m0) m0)→False
                      by (previous H2)
                      we proved False
                      we proceed by induction on the previous result to prove eq nat n (S m0)
                      we proved eq nat n (S m0)
∀H1:(le (S m0) n).(eq nat n (S m0))
          we proved (le m n)→(eq nat n m)
       we proved ∀n:nat.∀m:nat.(le n m)→(le m n)→(eq nat n m)