Theorem divisibilityNFoldPlus : forall z xs,
  0 <> z ->
    Forall (fun n => n mod z = 0) xs ->
      (fold_right plus 0 xs) mod z = 0.
Proof.
  (* Proof omitted for brevity; see Divisible.v for proofs. *)
Qed.
