proof(SafeBitset): DISCHARGE singletonZeroCapRejects via 2-arm Nat case-split (proven#90, #107) (#114)

\`\`\`idris
public export
singletonZeroCapRejects : (bit : Nat) -> singleton 0 bit = Nothing
singletonZeroCapRejects Z = Refl
singletonZeroCapRejects (S _) = Refl
\`\`\`

The OWED cited "abstract bit doesn't Refl-reduce" — correct for the
zero-arg version, but the case-split unblocks it:
- Z: \`compareNat 0 0 = EQ; EQ == LT = False\` → \`if False → Nothing\`
→ \`Refl\`
- S _: \`compareNat (S _) 0 = GT; GT == LT = False\` → same → \`Refl\`

Marginal "overly cautious OWED" (proven#107) — the comment was right
about the abstract-arg blocker but didn't suggest case-split as the
unblocker.

Refs #90 #107

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

Author: hyperpolymath