Goal:
    p : positive  IHp : Z.of_nat (Pos.to_nat p) = Z.pos p
  ============================
   (Z.pos (Pos.of_succ_nat (Pos.to_nat p)) = Z.pos (Pos.succ p))


DEBUG:Going to execute:
fun => <coq-core.plugins.cc::f_equal@0>