#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m normalize
[2,3,4: /4 width=1 by drop_skip_lt, drop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
#l #m #_ #_ #H <(le_n_O_to_eq … H) -H //
qed-.
lemma drop_O1_append_sn_le: ∀L1,L2,s,m. ⬇[s, 0, m] L1 ≡ L2 → m ≤ |L1| →
#L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m normalize
[2,3,4: /4 width=1 by drop_skip_lt, drop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ]
#l #m #_ #_ #H <(le_n_O_to_eq … H) -H //
qed-.
lemma drop_O1_append_sn_le: ∀L1,L2,s,m. ⬇[s, 0, m] L1 ≡ L2 → m ≤ |L1| →