mathlib3

[Merged by Bors] - feat(data/list/rdrop): drop or take from the right

#15475

Closed