DEFINITION leq_trans()
TYPE =
       ∀g:G.∀a1:A.∀a2:A.(leq g a1 a2)→∀a3:A.(leq g a2 a3)→(leq g a1 a3)
BODY =
Show proof