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