-* // [1,3: #L2 #I2 #V2 ] #l normalize
-[1,3: <plus_n_Sm #H destruct ]
-#H lapply (injective_plus_l … H) -H #HL12
-elim (ynat_cases l) /3 width=1 by lreq_zero/
-* /3 width=1 by lreq_succ/
+* // [1,3: #L2 #I2 #V2 ] #l
+[ #H elim (ysucc_inv_O_sn … H)
+| >length_pair >length_pair #H
+ lapply (ysucc_inv_inj … H) -H #HL12
+ elim (ynat_cases l) /3 width=1 by lreq_zero/
+ * /3 width=1 by lreq_succ/
+| #H elim (ysucc_inv_O_dx … H)
+]