proposition: Lemma nat_of_P_inj_iff (p q : positive): nat_of_P p = nat_of_P q <-> p = q.
proof: Proof. Proof with auto. split; intro. apply nat_of_P_inj... subst... Qed.
imports: Coq.Setoids.Setoid Coq.PArith.BinPos Coq.PArith.Pnat ZArith_base