calc _ < (neck :: tail).length := toDiffs_length_lt _ (by simp)
     _ = tail.length + 1 := by simp
as : List Int
head neck : Int
tail : List Int
h : head :: neck :: tail ≠ []
⊢ List.length (toDiffs (neck :: tail) (_ : ¬neck :: tail = [])).snd < List.length (neck :: tail)
no goals