List.le_eq_not_gt

theorem List.le_eq_not_gt : ∀ {α : Type u_1} [inst : LT α] (l₁ l₂ : List α), (l₁ ≤ l₂) = ¬l₂ < l₁

This theorem establishes a relation between the 'less than or equal to' (≤) operator and the 'greater than' (>) operator for lists in Lean 4. Specifically, it states that for any two lists `l₁` and `l₂` of a given type `α` which is equipped with a 'less than' (`<`) relation, `l₁` is less than or equal to `l₂` is equivalent to saying that `l₂` is not less than `l₁`.

More concisely: For lists `l₁` and `l₂` of type `α` with a total order `<`, the lists `l₁ ≤ l₂` and `l₂ > l₁` are equivalent.