verify(lean): one docstring on Books after the S5 and S7 merges

The S7 merge kept both branches' doc comments for the Books structure,
S5's (which names the sends) stranded above an unrelated theorem and
S7's on the structure; Lean refused the stray one. S5's text stays, on
the structure it describes. Kani's 52 harnesses verified in the same
run; only Lean's build stopped.

Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01HS8WZziDnyxunC23MUxrLp

verify/lean/Wanderbooks/Documents.lean

@@ -177,9 +177,6 @@ control guard requires of every entry a command posts. -/
 def Tagged (control : List Nat) (ls : List TLine) : Prop :=
   ∀ l ∈ ls, l.line.account ∈ control → l.doc ≠ none
 
-/-- The books: the control accounts (the receivables and payables roles),
-every posted line in order, and the sends recorded (each on its invoice;
-plan P4b S5). -/
 /-- A tagged list moves nothing that is unattached on a control account:
 no line it adds on one carries no document. -/
 theorem unattached_zero_of_tagged {control : List Nat} {e : List TLine} (h : Tagged control e)
@@ -202,8 +199,9 @@ def writeOffLines (control expense d D : Nat) (amount : Int) : List TLine :=
   [ { line := { account := control, side := .credit, amount := amount }, date := D, doc := some d },
     { line := { account := expense, side := .debit, amount := amount }, date := D, doc := none } ]
 
-/-- The books: the control accounts (the receivables and payables roles)
-and every posted line, in order. -/
+/-- The books: the control accounts (the receivables and payables roles),
+every posted line in order, and the sends recorded (each on its invoice;
+plan P4b S5). -/
 structure Books where
   control : List Nat
   lines : List TLine