## Stream: Is there code for X?

### Topic: le_or_le

#### Johan Commelin (Mar 04 2021 at 05:53):

Does it make sense to add this to mathlib? (I couldn't find it.)
I often find myself wanting to case on this, and invoking wlog every time is somewhat slow.

lemma le_or_le {α : Type*} [linear_order α] (a b : α) :
a ≤ b ∨ b ≤ a :=
(le_or_lt a b).imp id le_of_lt


#### Johan Commelin (Mar 04 2021 at 06:01):

Aah, the wonders of a predictable naming convention :rofl:

#### Kevin Buzzard (Mar 04 2021 at 07:19):

lt_irrefl is another one which takes some getting used to -- I would always look for not_lt_self.

#### Mario Carneiro (Mar 04 2021 at 07:22):

I think we already have le_or_ge, so I don't think it would be a bad idea to have le_or_le as an alias for le_total

#### Patrick Massot (Mar 04 2021 at 07:50):

I agree we could have aliases for both le_total and lt_irrefl.

#### Yury G. Kudryashov (Mar 04 2021 at 07:55):

We also have an alias docs#has_lt.lt.false

Last updated: May 17 2021 at 16:26 UTC