-lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| - l ≤ m → |L2| = l.
-#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m normalize
-[ /2 width=1 by le_n_O_to_eq/
-| #I #L #V #_ <minus_n_O #H elim (le_plus_xSy_O_false … H)
-| /3 width=2 by le_plus_to_le_r/
-| /4 width=2 by le_plus_to_le_r, eq_f/
+lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| - l ≤ m → yinj (|L2|) = l.
+#L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m
+[ #l #m #_ #H #_ normalize /2 width=1 by yle_inv_O2/
+| #I #L #V #_ normalize <yplus_inj #H elim (ylt_yle_false … H) -H //
+| #I #L1 #L2 #V #m #_ >yminus_inj >yminus_inj <minus_n_O <minus_n_O #IH #_ normalize
+ /3 width=2 by yle_inv_monotonic_plus_dx/
+| #I #L1 #L2 #V1 #v2 #l #m #_ #_ #IH
+ <yplus_inj <yplus_inj >yplus_SO2 >yplus_SO2 >yminus_succ
+ /4 width=1 by yle_inv_succ, eq_f/