Lemma sizePadModulo : forall n,
  ((sizePad n) + n) mod 16 = 0.
Proof.
  (** Proof omitted for brevity. *)
Qed.
