simp only [IsOrdered, List.pairwise_cons] at *
α : Type
inst✝ : LE α
a : α
xs : List α
h : IsOrdered xs
hle : ∀ x ∈ xs, a ≤ x
⊢ IsOrdered (a :: xs)
α : Type
inst✝ : LE α
a : α
xs : List α
h : List.Pairwise LE.le xs
hle : ∀ x ∈ xs, a ≤ x
⊢ (∀ a' ∈ xs, a ≤ a') ∧ List.Pairwise LE.le xs