Lemma sizePadRange : forall n,
  0 <= (sizePad n) < 16.
Proof.
  (** Proof omitted for brevity. *)
Qed.
