- elim (lift_inv_lref2 … Hi) -Hi * #Hil2 #H destruct
- [ -Hl12 lapply (lt_plus_to_lt_l … Hil2) -Hil2 #Hil2 /3 width=3 by lift_lref_lt, lift_lref_ge, ex2_intro/
- | -Hil1 >plus_plus_comm_23 in Hil2; #H lapply (le_plus_to_le_r … H) -H #H
- elim (le_inv_plus_l … H) -H #Hilm2 #Hm2i
- lapply (transitive_le … Hl12 Hilm2) -Hl12 #Hl12
+ elim (lift_inv_lref2 … Hi) -Hi * <yplus_inj #Hil2 #H destruct
+ [ -Hl12 lapply (ylt_inv_monotonic_plus_dx … Hil2) -Hil2 #Hil2 /3 width=3 by lift_lref_lt, lift_lref_ge, ex2_intro/
+ | -Hil1 >yplus_comm_23 in Hil2; #H lapply ( yle_inv_monotonic_plus_dx … H) -H #H
+ elim (yle_inv_plus_inj2 … H) -H >yminus_inj #Hl2im2 #H
+ lapply (yle_inv_inj … H) -H #Hm2i
+ lapply (yle_trans … Hl12 … Hl2im2) -Hl12 #Hl1im2