simp at *
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : IsOrdered l
⊢ IsOrdered (insert' a l)
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
l : List α
ordered : List.Pairwise LE.le l
⊢ List.Pairwise LE.le (insert' a l)