Theorem octet16LEtoBE : forall (z : Z),
  (octets16BE z) = List.rev (octets16LE z).
Proof.
  (** Proof omitted for brevity. *)
Qed.
