cases' n with n
case h
n : ℕ
h1 : ProblemPredicate n
⊢ ProblemPredicate' (n / 10) n
case h.zero
h1 : ProblemPredicate 0
⊢ ProblemPredicate' (0 / 10) 0

case h.succ
n : ℕ
h1 : ProblemPredicate (n + 1)
⊢ ProblemPredicate' ((n + 1) / 10) (n + 1)