Add Std.Queue (キュー) introduction

[Copilot]

Introduces Std.Queue, a persistent functional FIFO queue backed by two Lists, as a new entry in the Type section.

Changes

• LeanByExample/Type/Queue.lean — New file covering:

  • Internal structure (eList/dList and the invariant dList ++ eList.reverse)
  • Basic ops: isEmpty, enqueue, dequeue? with #guard_msgs-verified outputs
  • Dot-notation gotcha for enqueue (argument order)
  • do-notation chaining via popTwo example
  • Complexity notes (O(1) enqueue, amortized O(1) dequeue)
  • BFS on a binary tree as a canonical use case

• booksrc/SUMMARY.md — Added Queue: キュー entry between Prop and Quotient

-- dequeue? chains naturally with do-notation
def popTwo : Option (Nat × Nat) := do
  let q := ((∅ : Queue Nat).enqueue 10).enqueue 20
  let (x, q) ← q.dequeue?
  let (y, _) ← q.dequeue?
  return (x, y)
-- some (10, 20)