split_ifs can leave a hypothesis `h : False` that omega ignores

With nested ifs on Nat indices (e.g. nextIdx n i := if i = n + 2 then 0 else i + 1, then a goal about nextIdx n (nextIdx n e)), unfold nextIdx; split_ifs <;> omega failed with a bogus counterexample. In one branch, split_ifs had already simplified the inner condition 0 = n + 2 to False and kept it as a hypothesis h✝ : False, and omega does not use that hypothesis (it only collects linear arithmetic facts). Fix: split_ifs <;> first | omega | contradiction. To check, run all_goals trace_state after split_ifs. The unused-tactic linter tells you which call sites never need the contradiction.