DEFINITION llt_trans()
TYPE =
       ∀a1:A.∀a2:A.∀a3:A.(llt a1 a2)→(llt a2 a3)→(llt a1 a3)
BODY =
        assume a1: A
        assume a2: A
        assume a3: A
          we must prove (llt a1 a2)→(llt a2 a3)→(llt a1 a3)
          or equivalently (lt (lweight a1) (lweight a2))→(llt a2 a3)→(llt a1 a3)
          suppose H: lt (lweight a1) (lweight a2)
             we must prove (llt a2 a3)→(llt a1 a3)
             or equivalently (lt (lweight a2) (lweight a3))→(llt a1 a3)
             suppose H0: lt (lweight a2) (lweight a3)
                by (lt_trans . . . H H0)
                we proved lt (lweight a1) (lweight a3)
                that is equivalent to llt a1 a3
             we proved (lt (lweight a2) (lweight a3))→(llt a1 a3)
             that is equivalent to (llt a2 a3)→(llt a1 a3)
          we proved (lt (lweight a1) (lweight a2))→(llt a2 a3)→(llt a1 a3)
          that is equivalent to (llt a1 a2)→(llt a2 a3)→(llt a1 a3)
       we proved ∀a1:A.∀a2:A.∀a3:A.(llt a1 a2)→(llt a2 a3)→(llt a1 a3)