Commit 2024-07-25 07:50 36582f6c
View on Github →chore: deprecate sizeOf_dropSlice_lt (#15118)
As far as I can tell this lemma is not used anywhere. If it were needed somewhere, it would be better to proceed via Sublist in any case.
As a consolation prize I've added the simpler lemma length_dropSlice.