rw [insert', List.pairwise_cons]
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ List.Pairwise LE.le (insert' a [])
case nil
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a : α
ordered : List.Pairwise LE.le []
⊢ (∀ a' ∈ [], a ≤ a') ∧ List.Pairwise LE.le []