-| #n #H
- lapply (next_lt … Hh ((pr_next h)^n s2)) >H -H #H
- lapply (nlt_trans … H Hs12) -s1 #H1
- /3 width=5 by nlt_ge_false, nexts_le/ (* full auto too slow *)
+| #n #_ <sh_nexts_succ #H
+ lapply (sh_next_lt h Hh (⇡*[h,n]s2)) >H -H #H
+ lapply (nlt_trans … H … Hs12) -s1 #H1
+ /3 width=5 by nlt_ge_false, sh_nexts_le/ (* full auto too slow *)