- ∀s,n,d. deg o ((next h)^n s) (↑d) → deg o s (↑(d+n)).
-#h #o #H0 #s #n elim n -n normalize /3 width=3 by deg_inv_pred/
+ ∀s,n,d. deg o (⇡*[h,n]s) (↑d) → deg o s (↑(d+n)).
+#h #o #H0 #s #n @(nat_ind_succ … n) -n [ // ]
+#n #IH #d <sh_nexts_succ
+#H <nplus_succ_shift
+@IH -IH @(deg_inv_pred … H0) // (**) (* auto fails *)