proposition: Lemma positive_nat_N p : N.of_nat (Pos.to_nat p) = Npos p.
proof: Proof. destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat