match as with
| [] => exact False.elim (h rfl)
| _ :: [] => simp [toDiffs]
| head :: neck :: tail =>
  simp only [toDiffs]
  refine Nat.succ_lt_succ ?_
  calc _ < (neck :: tail).length := toDiffs_length_lt _ (by simp)
       _ = tail.length + 1 := by simp
as : List Int
h : as ≠ []
⊢ List.length (toDiffs as h).snd < List.length as
no goals