elim (IH1 … HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct
elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H
[ elim (ylt_yle_false … H) -H //
elim (IH1 … HLK1 HLK2) -IH1 /2 width=1 by/ #H #_ destruct
elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H
[ elim (ylt_yle_false … H) -H //