DEFINITION flt_arith1()
TYPE =
       ∀k1:K.∀c1:C.∀c2:C.∀t1:T.(cle (CHead c1 k1 t1) c2)→∀k2:K.∀t2:T.∀i:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef i))
BODY =
        assume : K
        assume c1: C
        assume c2: C
        assume t1: T
          we must prove (cle (CHead c1 __4 t1) c2)→∀k2:K.∀t2:T.∀i:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef i))
          or equivalently 
                le (plus (cweight c1) (tweight t1)) (cweight c2)
                  →K→∀t2:T.nat→(flt c1 t1 (CHead c2 __3 t2) (TLRef __1))
           suppose H: le (plus (cweight c1) (tweight t1)) (cweight c2)
           assume : K
           assume t2: T
           assume : nat
             (h1) 
                by (le_plus_l . .)
                we proved le (cweight c2) (plus (cweight c2) (tweight t2))
                by (le_lt_n_Sm . . previous)
                we proved lt (cweight c2) (S (plus (cweight c2) (tweight t2)))
lt (cweight c2) (plus (S O) (plus (cweight c2) (tweight t2)))
             end of h1
             (h2) 
                by (plus_sym . .)

                   eq
                     nat
                     plus (plus (cweight c2) (tweight t2)) (S O)
                     plus (S O) (plus (cweight c2) (tweight t2))
             end of h2
             by (eq_ind_r . . . h1 . h2)
             we proved lt (cweight c2) (plus (plus (cweight c2) (tweight t2)) (S O))
             by (le_lt_trans . . . H previous)
             we proved 
                lt
                  plus (cweight c1) (tweight t1)
                  plus (plus (cweight c2) (tweight t2)) (S O)
             that is equivalent to flt c1 t1 (CHead c2 __3 t2) (TLRef __1)
          we proved 
             le (plus (cweight c1) (tweight t1)) (cweight c2)
               →K→∀t2:T.nat→(flt c1 t1 (CHead c2 __3 t2) (TLRef __1))
          that is equivalent to (cle (CHead c1 __4 t1) c2)→∀k2:K.∀t2:T.∀i:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef i))
       we proved 
          K
            →∀c1:C.∀c2:C.∀t1:T.(cle (CHead c1 __4 t1) c2)→∀k2:K.∀t2:T.∀i:nat.(flt c1 t1 (CHead c2 k2 t2) (TLRef i))