proposition: Lemma nat_of_N_bij2 : forall n, N_of_nat (nat_of_N n) = n.
proof: Proof. intros [|p];simpl. reflexivity. assert (exists m, nat_of_P p = S m). induction p. rewrite nat_of_P_xI;eauto. rewrite nat_of_P_xO. destruct IHp as (m, Heq);rewrite Heq. simpl;eauto. unfold nat_of_P;simpl. eauto. destruct H as (m,Heq);rewrite Heq;simpl. assert (H:=pred_o_P_of_succ_nat_o_nat_of_P_eq_id p). rewrite <- H;rewrite Heq. simpl. rewrite Pos.pred_succ. trivial. Qed.
imports: Coq(ZArith)