have h2 : 10 ^ 3 ≤ 10 * n := by
  rw [← h1.left]
  refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
  simp
n : ℕ
h1 : ProblemPredicate n
⊢ 100 ≤ n
n : ℕ
h1 : ProblemPredicate n
h2 : 10 ^ 3 ≤ 10 * n
⊢ 100 ≤ n