DEFINITION llt_repl()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.(llt a1 a3)→(llt a2 a3)
BODY =
        assume g: G
        assume a1: A
        assume a2: A
        suppose H: leq g a1 a2
        assume a3: A
          we must prove (llt a1 a3)→(llt a2 a3)
          or equivalently (lt (lweight a1) (lweight a3))→(llt a2 a3)
          suppose H0: lt (lweight a1) (lweight a3)
             (H1) 
                by (lweight_repl . . . H)
                we proved eq nat (lweight a1) (lweight a2)
                we proceed by induction on the previous result to prove lt (lweight a2) (lweight a3)
                   case refl_equal : ⇒
                      the thesis becomes the hypothesis H0
lt (lweight a2) (lweight a3)
             end of H1
             consider H1
             we proved lt (lweight a2) (lweight a3)
             that is equivalent to llt a2 a3
          we proved (lt (lweight a1) (lweight a3))→(llt a2 a3)
          that is equivalent to (llt a1 a3)→(llt a2 a3)
       we proved ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.(llt a1 a3)→(llt a2 a3)