-#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <plus_n_Sm ] (**) (* full auto fails *)
-[ /3 width=7 by fcla_next, sor_pn, max_S2_le_S, le_S_S, ex4_2_intro/
-| /4 width=7 by fcla_next, sor_nn, le_S, le_S_S, ex4_2_intro/
+#f2 #n2 #Hf2 elim (IH … Hf2) -IH -Hf2 -Hf1 [2,4: #f #n <nplus_succ_dx ] (**) (* full auto fails *)
+[ /3 width=7 by fcla_next, sor_pn, nle_max_sn_succ_dx, nle_succ_bi, ex4_2_intro/
+| /4 width=7 by fcla_next, sor_nn, nle_succ_dx, nle_succ_bi, ex4_2_intro/