| #i #l1 #m2 #Hil1 #l2 #m1 #Hl12 #_ #_
lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #_ #Hl21 #Hm12
lapply (transitive_le … (i+m1) Hl21 ?) /2 width=1 by monotonic_le_plus_l/ -Hl21 #Hl21
>(plus_minus_m_m m2 m1 ?) /3 width=3 by lift_lref_ge, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #Hl12 #_ #_
lapply (lt_to_le_to_lt … Hil1 Hl12) -Hl12 #Hil2 /4 width=3 by lift_lref_lt, ex2_intro/
| #i #l1 #m2 #Hil1 #l2 #m1 #_ #Hl21 #Hm12
lapply (transitive_le … (i+m1) Hl21 ?) /2 width=1 by monotonic_le_plus_l/ -Hl21 #Hl21
>(plus_minus_m_m m2 m1 ?) /3 width=3 by lift_lref_ge, ex2_intro/