| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct -T2
[ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
| -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
@(ex2_1_intro … #(i - e2))
[ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ]
| #i #d1 #e1 #Hid1 #d2 #e2 #T2 #Hi #Hd12
elim (lift_inv_lref2 … Hi) -Hi * #Hid2 #H destruct -T2
[ -Hd12; lapply (lt_plus_to_lt_l … Hid2) -Hid2 #Hid2 /3/
| -Hid1; lapply (arith1 … Hid2) -Hid2 #Hid2
@(ex2_1_intro … #(i - e2))
[ >le_plus_minus_comm [ @lift_lref_ge @(transitive_le … Hd12) -Hd12 /2/ | -Hd12 /2/ ]