-elim n1 -n1
-[ #s * [ // ] #n2 >iter_O #H
- elim (lt_refl_false s) >H in ⊢ (??%); -H
- /2 width=1 by nexts_lt/
-| #n1 #IH #s *
- [ >iter_O #H -IH
- elim (lt_refl_false s) <H in ⊢ (??%); -H
- /2 width=1 by nexts_lt/
- | #n2 >iter_S >iter_S <(iter_n_Sm … (next h)) <(iter_n_Sm … (next h)) #H
- /3 width=2 by eq_f/
+@(nat_ind_succ … n1) -n1
+[ #s #n2 @(nat_ind_succ … n2) -n2 [ // ] #n2 #_ <sh_nexts_zero #H
+ elim (nlt_inv_refl s) >H in ⊢ (??%); -H
+ /2 width=1 by sh_nexts_lt/
+| #n1 #IH #s #n2 @(nat_ind_succ … n2) -n2
+ [ <sh_nexts_zero #H -IH
+ elim (nlt_inv_refl s) <H in ⊢ (??%); -H
+ /2 width=1 by sh_nexts_lt/
+ | #n2 #_ <sh_nexts_succ <sh_nexts_succ >sh_nexts_swap >sh_nexts_swap #H
+ lapply (IH … H) -IH -H //