- | * #J #K #W #j #Hlj #Hji #HLK #HnW
- elim (yle_inv_succ1 … Hlj) -Hlj #Hlj #Hj
- lapply (ylt_O … Hj) -Hj #Hj
- lapply (drop_inv_drop1_lt … HLK ?) // -HLK #HLK
- >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
- #HnU1 <minus_le_minus_minus_comm in HnW;
- /5 width=9 by nlift_bind_dx, monotonic_lt_pred, lt_plus_to_minus_r, ex5_4_intro, or_intror/
+ | * #J #K #W #j #Hlj elim (yle_inv_succ1 … Hlj) -Hlj #Hlj #Hj
+ <Hj >yminus_succ #Hji #HLK #HnW
+ lapply (drop_inv_drop1_lt … HLK ?) /2 width=1 by ylt_O/ -HLK #HLK
+ <yminus_SO2 in Hlj; #Hlj #H4
+ @or_intror @(ex5_4_intro … HLK) (**) (* explicit constructors *)
+ /3 width=9 by nlift_bind_dx, ylt_pred, ylt_inj/