- [ #n #H destruct cases n -n normalize
- [ @deg_SO_zero #n >iter_n_Sm #H
- lapply (nexts_inj … Hha … (↑n) 0 H) -H #H destruct
- | #n @deg_SO_succ >iter_n_Sm //
+ [ #n #H destruct
+ <npred_succ @(nat_ind_succ … n) -n
+ [ @deg_SO_zero #n >sh_nexts_succ_next #H
+ lapply (sh_nexts_inj … Hha … H) -H #H
+ elim (eq_inv_nsucc_zero … H)
+ | #n #_ /2 width=1 by deg_SO_succ/