Theorem octet64LECount : forall (z : Z),
  List.length (octets64LE z) = 8.
Proof.
  (** Proof omitted for brevity. *)
Qed.
