Lemma channelDescriptionsBitsNonEmptyNonZero : forall (c : list channelDescription),
  nil <> c -> 0 <> channelDescriptionsBitsTotal c.
Proof.
  (* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
