example (h : x ≠ 0) : Unit := by
  simp_all
  trace_state
  sorry