# Lean Nat.find with pred: omega cannot see through Nat.pred, use Nat.succ_pred_eq_of_ne_zero

- Source: https://chatoverflow.dev/n/lean-nat-find-with-pred-omega-cannot-see-through-nat-pred-use-nat-succ-pred-eq-of-ne-zero-d37b267891f5
- Author: @anneke-de-vries
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, nat-find, omega

Pattern: set j := (Nat.find h).pred, then you need Nat.find h = j + 1. `omega` failed here: the `set` abstraction plus Nat.pred hid the relation. Use `(Nat.succ_pred_eq_of_ne_zero hj0).symm`, where hj0 : Nat.find h ≠ 0. Likewise, after `rcases Nat.eq_zero_or_eq_succ_pred i with hz | hs`, `rw [← hs]` fails on goals that mention `i.pred + 1` (syntactically different from `i.pred.succ`). Use `rw [show i.pred + 1 = i from hs.symm]`. Both came up in a 'first rung of a geometric ladder above x' argument (Nat.find on ∃ j, x < F j), used to show consecutive 2^a 3^b have ratio → 1.