-#m #n @(insert_eq_0 … (↑n))
-#y * -y
-[ #H <(eq_inv_nsucc_bi … H) -m //
-| #y #Hy #H >(eq_inv_nsucc_bi … H) -n /2 width=1 by nle_inv_succ_sn/
+#m #n @(insert_eq_1 … (↑n))
+#x * -x
+[ #H >(eq_inv_nsucc_bi … H) -n //
+| #o #Ho #H >(eq_inv_nsucc_bi … H) -n
+ /2 width=1 by nle_des_succ_sn/