constructor
case pos
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ (∀ a' ∈ x :: xs, a ≤ a') ∧ List.Pairwise LE.le (x :: xs)
case pos.left
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ ∀ a' ∈ x :: xs, a ≤ a'

case pos.right
α : Type
hl : LinearOrder α
inst✝ : DecidableRel LE.le
a x : α
xs : List α
ih : List.Pairwise LE.le xs → List.Pairwise LE.le (insert' a xs)
ordered : List.Pairwise LE.le (x :: xs)
h : a ≤ x
⊢ List.Pairwise LE.le (x :: xs)