abi: close TacticRecord round-trip lemmas (natToFinToNat, clampRoundtripInRange)

[hyperpolymath]

Deferred in PR #151 (`feat(abi): EchidnaABI.TacticRecord`).

Problem

`src/abi/EchidnaABI/TacticRecord.idr` ships the comparison total-order proofs (refl + antisym) constructively but documents two round-trip lemmas as deliberately unclosed:

• `natToFinToNat : (m : Nat) -> (p : LT m (S MaxConfidence)) -> finToNat (natToFinLT m {prf = p}) = m`
• `clampRoundtripInRange : (n : Nat) -> (prf : LT n (S MaxConfidence)) -> finToNat (clampConfidence n) = n`

Both require an LTE-weakening step on the nat side (LTE n m → LTE n (S m)) that hasn't been spelled out structurally. The module ships without `believe_me` or admits — the absence is explicit, not silent.

Acceptance

• Both lemmas typecheck under `idris2 --check` (standalone) with zero believe_me / postulate / admit.
• Module docstring updated to remove the Wave-3 deferral note.
• `echidnaabi.ipkg` full-package build status unchanged (currently red on the documented `EchidnaABI.Foreign` owner-managed state, NOT on this module).

[hyperpolymath]

Closing as duplicate of #152 (same scope: natToFinToNat + clampRoundtripInRange round-trip lemmas in src/abi/EchidnaABI/TacticRecord.idr).

#152 was filed first and has identical scope. Consolidating discussion there.