proposition: Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
proof: Proof. induction n as [|n H]; trivial. - now destruct 1. - intros _. simpl Pos.of_nat. destruct n. + trivial. + rewrite Pos2Nat.inj_succ. f_equal. now apply H. Qed.
imports: BinPos PeanoNat