Theorem channelLayoutPackingBitsDiv8 : ∀ c, divisible8 (channelLayoutPackingBits (c)).
Proof.
  (* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
