DEFINITION lt_le_e()
TYPE =
       ∀n:nat.∀d:nat.∀P:Prop.((lt n d)→P)→((le d n)→P)→P
BODY =
Show proof