proof(SafeCBOR): DISCHARGE maxNestingDepthAnchor via Refl (proven#90, #107) (#110)

Per [proven#107](#107)
"overly cautious OWED" pattern — Nat-literal variant.

\`\`\`idris
public export
maxNestingDepthAnchor : MaxNestingDepth = 64
maxNestingDepthAnchor = Refl
\`\`\`

\`MaxNestingDepth\` is \`public export\` with body \`64\` (SafeCBOR.idr
L150-152). Both sides are the same \`Nat\` literal — \`Refl\` closes
without unary expansion. Same pattern as the SafeArchive PR.

Refs #90 #107

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/Proven/SafeCBOR/Proofs.idr

@@ -217,6 +217,9 @@ emptyMapNoDupes = Refl
 -- OWED
 --------------------------------------------------------------------------------
 
-||| OWED: `MaxNestingDepth = 64`. Blocked on Nat-literal opacity.
+||| DISCHARGED: `MaxNestingDepth = 64`. `MaxNestingDepth` is `public
+||| export` with body `64` (SafeCBOR.idr L150-152). Both sides are
+||| the same `Nat` literal — `Refl` closes without unary expansion.
 public export
-0 maxNestingDepthAnchor : MaxNestingDepth = 64
+maxNestingDepthAnchor : MaxNestingDepth = 64
+maxNestingDepthAnchor = Refl