1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9

-- Ah darn this no longer works with Lean v4.22

example : False := by
  let getHeartbeats (x : Nat) : Nat :=
    let .ok _ state := IO.mkRef x ()  -- ensure `x` is not eliminated
    let .ok val state := IO.getNumHeartbeats state
    val
  have : getHeartbeats 0 ≠ getHeartbeats (0 + 1 - 1) := by native_decide
  simp [getHeartbeats] at this