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