Lemma fold_right_add_cons : forall x xs,
  x + fold_right plus 0 xs = fold_right plus 0 (x :: xs).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
