Theorem divisiblityNAdd : forall (x y z : nat),
  0 <> z -> x mod z = 0 -> y mod z = 0 -> (x + y) mod z = 0.
Proof.
  (* Proof omitted for brevity; see Divisible.v for proofs. *)
Qed.
