Order on a quotient group

Stream: Is there code for X?

[Yaël Dillies]

I'm readin The Sperner Property, Griggs, and it mentions this order on a quotient group:

The quotient of a ranked poset P under a group of (order-preserving) automorphisms G is denoted by P/G. Its elements are the orbits of P under G, ordered by A ≤ B in P/G if there exist a ∈ A, b ∈ B such that a ≤ b in P.

Do we have this order in mathlib?