#h #Hh #s #n elim n -n [ // ] normalize #n #IH
lapply (next_lt … Hh ((next h)^n s)) #H
lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/
qed.
#h #Hh #s #n elim n -n [ // ] normalize #n #IH
lapply (next_lt … Hh ((next h)^n s)) #H
lapply (le_to_lt_to_lt … IH H) -IH -H /2 width=2 by lt_to_le/
qed.