case nil
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
h : ¬x ∈ []
⊢ nextOr ([] ++ [x]) x d = d

case cons
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
z : α
zs : List α
IH : ¬x ∈ zs → nextOr (zs ++ [x]) x d = d
h : ¬x ∈ z :: zs
⊢ nextOr (z :: zs ++ [x]) x d = d
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h : ¬x ∈ xs
⊢ nextOr (xs ++ [x]) x d = d
induction' xs with z zs IH
no goals
case nil
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
h : ¬x ∈ []
⊢ nextOr ([] ++ [x]) x d = d
simp
case cons.intro
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
z : α
zs : List α
IH : ¬x ∈ zs → nextOr (zs ++ [x]) x d = d
h : ¬x ∈ z :: zs
hz : ¬x = z
hzs : ¬x ∈ zs
⊢ nextOr (z :: zs ++ [x]) x d = d
case cons
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
z : α
zs : List α
IH : ¬x ∈ zs → nextOr (zs ++ [x]) x d = d
h : ¬x ∈ z :: zs
⊢ nextOr (z :: zs ++ [x]) x d = d
obtain ⟨hz, hzs⟩ := not_or.mp (mt mem_cons.2 h)
no goals
case cons.intro
α : Type u_1
inst✝ : DecidableEq α
xs : List α
x d : α
h✝ : ¬x ∈ xs
z : α
zs : List α
IH : ¬x ∈ zs → nextOr (zs ++ [x]) x d = d
h : ¬x ∈ z :: zs
hz : ¬x = z
hzs : ¬x ∈ zs
⊢ nextOr (z :: zs ++ [x]) x d = d
rw [cons_append, nextOr_cons_of_ne _ _ _ _ hz, IH hzs]