Definition asMultipleOf4 (size : nat) : nat :=
  asMultipleOf size 4 p0not4.
