uniqe_succ.v

Require Import PArith Omega.

Lemma unique_succ : forall a : positive, exists! b : nat, S b = Pos.to_nat a.
Proof.
  induction a.
  - destruct IHa as [b [Hb Hbunique]].
    rewrite Pos2Nat.inj_xI. 
    eexists.
    split; eauto.
    intros. omega.
  - destruct IHa as [b [Hb Hbunique]].
    rewrite Pos2Nat.inj_xO.
    rewrite <- Hb.
    simpl.
    eexists.
    split; eauto.
    intros. omega.
  - exists 0. split; auto.
    compute. intros. omega.
Qed.