| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
| #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12