Natural - using binary

Fixpoint natbin_inc2 (n : natbin) : natbin :=
  match n with
  | Z     =>  I Z
  | P Z   =>  I Z
  | P n'   =>  I n'
  | I Z   =>  P (I Z)
  | I n'  =>  P (natbin_inc2 n')
  end
.
Compute natbin_inc2(natbin_inc2(Z)).  (* 2 *)
Compute natbin_inc2(natbin_inc2(natbin_inc2(Z))).
Compute natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(Z)))).
Compute natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(Z))))).
Compute natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(Z)))))).
Compute natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(Z))))))).
Compute natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(Z)))))))).
Compute natbin_inc2(
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
          natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
            Z
          ))))
        ))))
        ).
Compute natbin_inc2(natbin_inc2(  (* 10 *)
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
          natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
            Z
          ))))
        ))))
        )).
Compute natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2( (* 12 *)
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
          natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
            Z
          ))))
        ))))
        )))).
Compute
        natbin_inc2(natbin_inc2(natbin_inc2(  (* 15 *)
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
          natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
            Z
          ))))
        ))))
        ))))
        ))).
Compute
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(  (* 16 *)
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
        natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
          natbin_inc2(natbin_inc2(natbin_inc2(natbin_inc2(
            Z
          ))))
        ))))
        ))))
        )))).