Lemma divisiblity8Add : forall (x y : nat),
  divisible8 x -> divisible8 y -> divisible8 (x + y).
Proof.
  (* Proof omitted for brevity; see ChannelDescription.v for proofs. *)
Qed.
