case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)

case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
n m : ℕ
⊢ Chain' (fun a b => b = succ a) (Ico n m)
by_cases n < m
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (n :: Ico (n + 1) m)
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
rw [eq_cons h]
no goals
case pos
n m : ℕ
h : n < m
⊢ Chain' (fun a b => b = succ a) (n :: Ico (n + 1) m)
exact chain_succ_range' _ _ 1
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) []
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) (Ico n m)
rw [eq_nil_of_le (le_of_not_gt h)]
no goals
case neg
n m : ℕ
h : ¬n < m
⊢ Chain' (fun a b => b = succ a) []
trivial