- elim (yle_inv_succ1 … Hli) -Hli
- #Hli #Hi <Hi >yplus_succ1 #H lapply (ylt_inv_succ … H) -H
- #Hilm lapply (drop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O/
- #HLK1 elim (IHL12 … HLK1) -IHL12 -HLK1 <yminus_inj >yminus_SO2
- /4 width=3 by ylt_O, drop_drop_lt, ex2_intro/
+ elim (yle_inv_succ_sn_lt … Hli) -Hli #Hli #Hi
+ lapply (ylt_inv_inj … Hi) -Hi #Hi
+ <(S_pred … Hi) >yplus_succ1 <ysucc_inj #H
+ lapply (ylt_inv_succ … H) -H #Hilm
+ lapply (drop_inv_drop1_lt … HLK2 Hi) -HLK2 #HLK1
+ elim (IHL12 … HLK1) -IHL12 -HLK1 >minus_SO_dx
+ /3 width=3 by drop_drop_lt, ex2_intro/