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

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.