Lemma fold_right_1_length : forall xs,
  Forall (eq 1) xs -> fold_right add 0 xs = length xs.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
