-lemma deg_inv_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
-#h #g #k #l @(nat_ind_plus … l) -l //
-#l #IHl #l0 >iter_SO #H
-lapply (deg_inv_pred … H) -H <(associative_plus l0 1 1) #H
-lapply (IHl … H) -IHl -H //
+lemma deg_inv_prec: ∀h,g,k,d,d0. deg h g ((next h)^d k) (d0+1) → deg h g k (d+d0+1).
+#h #g #k #d @(nat_ind_plus … d) -d //
+#d #IHd #d0 >iter_SO #H
+lapply (deg_inv_pred … H) -H <(associative_plus d0 1 1) #H
+lapply (IHd … H) -IHd -H //