It's definitely redundant. I don't know if this redundancy is accidental or intentional. How do other headers do it?

We explicitly say that <compare> is included in every header that needs it, so it's clear that the comparisons using it (and other comparisons using those) are well-formed.

I see no reason to "optimize" that by removing it where it's already implicitly included. What benefit would it have? It wouldn't make anything clearer.

Implementations are free to not re-include it unnecessarily, the difference is not observable.

We explicitly say that <compare> is included in every header that needs it, so it's clear that the comparisons using it (and other comparisons using those) are well-formed.

Thank you. I think this is a clear reason to me that we should not remove #include <compare> even if it is redundant.