Theorem channelLayoutDescriptionBitsLe8 : forall (c : channelLayoutDescription),
  8 <= channelLayoutDescriptionBits c.
Proof.
  (* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
