-[ * [1,3: /3 width=2/ ] #i #d #e
- elim (lt_dec i d) #Hid
- [ /4 width=2/
- | lapply (false_lt_to_le … Hid) -Hid #Hid
- elim (lt_dec i (d + e)) #Hide
- [ @or_intror * #T1 #H
- elim (lift_inv_lref2_be … H Hid Hide)
- | lapply (false_lt_to_le … Hide) -Hide /4 width=2/
+[ * [1,3: /3 width=2 by lift_sort, lift_gref, ex_intro, or_introl/ ] #i #d #e
+ elim (lt_or_ge i d) #Hdi
+ [ /4 width=3 by lift_lref_lt, ex_intro, or_introl/
+ | elim (lt_or_ge i (d + e)) #Hide
+ [ @or_intror * #T1 #H elim (lift_inv_lref2_be … H Hdi Hide)
+ | -Hdi /4 width=2 by lift_lref_ge_minus, ex_intro, or_introl/