Theorem fold_right_add_app : forall xs ys,
  fold_right add 0 xs + fold_right add 0 ys = fold_right add 0 (xs ++ ys).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
