Mathlib.Data.Int.ConditionallyCompleteOrder._auxLemma.1

theorem Mathlib.Data.Int.ConditionallyCompleteOrder._auxLemma.1 : ∀ {α : Type u} [inst : LE α] {x y : α}, (x ≥ y) = (y ≤ x)

This theorem states that for any type `α` that has a less than or equal to (`≤`) operation, and for any two elements `x` and `y` of that type, `x` is greater than or equal to (`≥`) `y` if and only if `y` is less than or equal to (`≤`) `x`. This is a fundamental property of ordered sets in mathematics.

More concisely: For all types `α` with a `≤` operation and all `x, y` in `α`, `x ≥ y` if and only if `y ≤ x`.