feat(order/antichain): Strong antichains (#11400)
This introduces a predicate `is_strong_antichain` to state that a set is a strong antichain with respect to a relation.
`s` is a strong (upward) antichain wrt `r` if for all `a ≠ b` in `s` there is some `c` such that `¬ r a c` or `¬ r b c`. A strong downward antichain of the swapped relation.
