constructor
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1 ∧ List.length (split cs).snd ≤ List.length cs + 1
case left
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).fst ≤ List.length cs + 1

case right
α : Type
inst✝¹ : LE α
inst✝ : DecidableRel LE.le
x y : α
zs : List α
a b : α
cs : List α
helper : List.length (split cs).fst ≤ List.length cs ∧ List.length (split cs).snd ≤ List.length cs
⊢ List.length (split cs).snd ≤ List.length cs + 1