α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x ≤ y
rw [le_iff_lt_or_eq]
no goals
α : Type u_1
inst✝ : LinearOrderedField α
x y : α
⊢ const x ≤ const y ↔ x < y ∨ x = y
exact or_congr const_lt const_equiv