replace :=
  searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) rfl
    (by norm_num <;> decide)
n : ℕ
this : SearchUpTo 90 990
⊢ ProblemPredicate n → SolutionPredicate n
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n