Data.List.Rotate mathlib#1490

Stream: mathlib4

[Jihoon Hyun]

#1490 contains a bunch of nthLe theorems, and most of them are deprecated. I tried to change it to non-deprecated theorems, but could only find out that leaving them as is is a nice choice. How do you think about this issue?

[Mario Carneiro]

theorems with deprecated constants in the statement should also be deprecated

[Mario Carneiro]

If the statement does not use deprecated constants, you can try removing them from the proof but this is not required