Precedes and succeeds under relation (Proposal 10)

[T0mstone]

Unicode defines curlier variants of U+227A ≺ PRECEDES and U+227B ≻ SUCCEEDS. For more context, see the discussion on Discord.

This is related to, but not dependent on, nor incompatible with, #42.

[MDLC01]

The current state of this PR is that is is blocked on #155. The reason is that this PR uses the .curly modifier on prec and succ with a different meaning compared to the existing prec.curly.eq and succ.curly.eq. Those names are deprecated and renamed to prec.eq.slant and succ.eq.slant respectively in #155.

Theoretically, we could merge this PR before #155 without causing any breakage (except for people who relied on prec.curly and succ.curly falling back to prec.curly.eq and succ.curly.eq respectively), but the main reason we don't do it is because it doesn't feel right for the same modifier to have two meanings on the same base symbol.

Once #155 is merged, we need to decide whether we want to merge this immediately, or if we wait for a release to be made in between in order to ensure users relying on the aforementioned fallback see a proper deprecation message.