proposition: Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n.
proof: Proof. destruct n as [|p]; trivial. simpl. destruct (Pos2Nat.is_succ p) as (m,H). rewrite H. simpl. f_equal. now apply SuccNat2Pos.inv. Qed.
imports: Arith_base BinPos BinInt BinNat Pnat Nnat