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:
f_equal
DEBUG LTAC Evaluated term: Pos2Nat.inj_succ
DEBUG LTAC Evaluated term: Pos2Nat.inj_succ