GP was likely refering to extraordinary disks with more than 7200 rpm
10KRPM SAS drives in my SAN.
The parent comment said no one uses drives strictly faster than 7200.
Pretty sure 10K RPM drives are used too.
I have no opinion on the matter, just pointing out that your comment doesn't follow from the previous one. But I imagine that when they said "nobody" uses faster disks, they were exaggerating a bit. The question is whether the default set of "latency numbers everyone should know" should reference SSDs or uncommon spinning disks.
They're used, but rare because they got to a weird position in between slower drives that are cheaper to produce and operate and SSDs. E.g. 15K RPM drives were a thing but while you can still buy some models they're typically more expensive than SSDs, so you mostly buy them to replace drives in existing arrays.