DEFINITION well_founded_ltof()
TYPE =
       ∀A:Set.∀f:A→nat.(well_founded A (ltof A f))
BODY =
        assume A: Set
        assume f: A→nat
          (H) 
             we must prove ∀n:nat.(λn0:nat.∀a:A.(lt (f a) n0)→(Acc A (ltof A f) a) n)
             or equivalently ∀n:nat.∀a:A.(lt (f a) n)→(Acc A (ltof A f) a)
             assume n: nat
                we proceed by induction on n to prove ∀a:A.(lt (f a) n)→(Acc A (ltof A f) a)
                   case O : ⇒
                      the thesis becomes ∀a:A.(lt (f a) O)→(Acc A (ltof A f) a)
                          assume a: A
                          suppose H: lt (f a) O
                            (H0) consider H
                            (H1) 
                               by (lt_n_O .)
not (lt (f a) O)
                            end of H1
                            suppose H2: lt (f a) O
                               by (H1 H2)
                               we proved False
                            we proved (lt (f a) O)→False
                            by (previous H0)
                            we proved False
                            we proceed by induction on the previous result to prove Acc A (ltof A f) a
                            we proved Acc A (ltof A f) a
∀a:A.(lt (f a) O)→(Acc A (ltof A f) a)
                   case S : n0:nat ⇒
                      the thesis becomes ∀a:A.∀ltSma:(lt (f a) (S n0)).(Acc A (ltof A f) a)
                      (IHn) by induction hypothesis we know ∀a:A.(lt (f a) n0)→(Acc A (ltof A f) a)
                          assume a: A
                          suppose ltSma: lt (f a) (S n0)
                            assume b: A
                               we must prove (ltof A f b a)→(Acc A (ltof A f) b)
                               or equivalently (lt (f b) (f a))→(Acc A (ltof A f) b)
                               suppose ltfafb: lt (f b) (f a)
                                  by (lt_n_Sm_le . . ltSma)
                                  we proved le (f a) n0
                                  by (lt_le_trans . . . ltfafb previous)
                                  we proved lt (f b) n0
                                  by (IHn . previous)
                                  we proved Acc A (ltof A f) b
                               we proved (lt (f b) (f a))→(Acc A (ltof A f) b)
                               that is equivalent to (ltof A f b a)→(Acc A (ltof A f) b)
                            we proved ∀b:A.(ltof A f b a)→(Acc A (ltof A f) b)
                            by (Acc_intro . . . previous)
                            we proved Acc A (ltof A f) a
∀a:A.∀ltSma:(lt (f a) (S n0)).(Acc A (ltof A f) a)
                we proved ∀a:A.(lt (f a) n)→(Acc A (ltof A f) a)
             we proved ∀n:nat.∀a:A.(lt (f a) n)→(Acc A (ltof A f) a)
∀n:nat.(λn0:nat.∀a:A.(lt (f a) n0)→(Acc A (ltof A f) a) n)
          end of H
          assume a: A
             by (le_n .)
             we proved le (S (f a)) (S (f a))
             that is equivalent to lt (f a) (S (f a))
             by (H . . previous)
             we proved Acc A (ltof A f) a
          we proved ∀a:A.(Acc A (ltof A f) a)
          that is equivalent to well_founded A (ltof A f)
       we proved ∀A:Set.∀f:A→nat.(well_founded A (ltof A f))