Definition asMultipleOf16 (size : nat) : nat :=
  asMultipleOf size 16 p0not16.
