[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
elim (ylt_split i d) #Hdi [ -H | -HL ]
[ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/
[ #I #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #d #HL #H
elim (ylt_split i d) #Hdi [ -H | -HL ]
[ <(ymax_pre_sn d (⫯i)) /2 width=1 by ylt_fwd_le_succ/