Cardano Updates

for bug report see https://github.com/agda/agda/issues/8532

For consistency with SUBUTXOW

for bug report see https://github.com/agda/agda/issues/8532

Proves by induction on the SUBLEDGERS transition that the UTxO-state
coin total at the start of a sub-tx batch plus all outs + donations
equals the UTxO coin total at the end plus all consumed spend inputs
(compared against the batch-start snapshot `utxo₀`):

```agda
getCoin (UTxOStateOf s₀) + Σ (cbalance (outs stx) + DonationsOf stx)
≡ getCoin (UTxOStateOf s₁) + Σ cbalance (utxo₀ ∣ SpendInputsOf stx)
```

Base case (`BS-base Id-nop`): both sides reduce to `x + 0`, so `refl`.
Inductive case: `SUBLEDGER-I` is impossible under `isTopLevelValid ≡
true`; `SUBLEDGER-V` combines the per-step SUBUTXOW balance with the
IH via an eight-step +-commutative-monoid rearrangement.

Introduces `subutxow-step-coin` as a new module parameter:

```agda
getCoin s₀ + cbalance (outs stx) + DonationsOf stx
≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx)
```

+  Rationale for keeping this as a parameter at the SUBLEDGERS level:
   proving it locally requires, beyond `balance-∪` and `split-balance`,
   two batch-wide invariants:

   1. the running UTxO agrees with `utxo₀` on every sub-tx's spend
      inputs, and
   2. freshness of each sub-tx's TxId relative to the running UTxO

   neither of which is a local SUBUTXO premise; both follow from
   batch-wide disjointness exposed by the outer UTXO rule and will be
   discharged in a follow-up PR dedicated to general Dijkstra PoV
   infrastructure.

Statement parallels the existing `SUBLEDGERS-certs-pov`, uses
`SubLedgerEnv.utxo₀ Γ` uniformly on the RHS (matching the shape of
`batch-balance-coin`), and is the key lemma needed to derive
`batch-utxo-accounting` internally in the next step of this PR.

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module
parameters of `Utxo/Properties/PoV` with direct proofs.  The proofs are
organised as three layers:

+  Layer 1 — single-transaction coin equations

   `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)`

   `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)`

   Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin`
   across `+`, followed by `coin∘inject≗id` to strip each `inject`.  The
   consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel
   the mint term (from UTXO premise p₆ / SUBUTXO premise).

+  Layer 2 — sum-over-sub-transactions coin equations

   `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over
   `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from
   `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction.

   `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx`
   hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`)
   through the induction so each element's Layer-1 application has its
   `noMint` premise available.

+  Layer 3 — the two batch-level coin equations

   `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer
   `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by
   repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1
   top-level equation for the top-level summand, and substitute the Layer-2
   equation for the sub-transaction sum.

   The produced-side proof ends with a small associative-commutative shuffle
   (`reshape-top`) that reorders the top-level fields from
   `(outs + Donations + DirectDeposits) + TxFees` to the stated
   `outs + TxFees + Donations + DirectDeposits`.  The shuffle uses the same
   `swap-right` helper already used in `UTXO-V-mechanical`.

+  Supporting change

   Adds a small helper alias `noMintingSubTxs` at the top of the file to keep
   the sub-level mint-conservation hypothesis readable in the theorem
   statements.

All proofs typecheck under `--safe`.  The `UTXO-pov` placeholder remains;
this commit delivers the coin-balance infrastructure that the eventual
full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will
depend on.

State and partially prove the Dijkstra LEDGER preservation-of-value
theorem with the corrected HasCoin-LedgerState that includes deposits.

- LEDGER-I (invalid case): Fully proved via utxow-pov-invalid.
- LEDGER-V (valid case): Equational chain with holes, to be filled.

The HasCoin-LedgerState total is:
  getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState)

Key insight: SUBLEDGERS-pov cannot be proved independently because
individual SUBUTXO rules have no balance premise — only the batch-level
consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof
must reason about the entire step at once.

Add the applyWithdrawals preservation-of-value proof machinery and
prove several lemmas that were previously assumed as module parameters
in Conway.

New proofs in Ledger.Prelude (previously Conway module parameters):
- indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ
- sumConstZero: getCoin (constMap X 0) ≡ 0
- getCoin-cong: indexedSum' proj₂ respects set equality
- res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ))
- getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom,
  ∪ˡsingleton0≡: singleton map getCoin lemmas
- indexedSumL-proj₂-zero: sum of zero-valued entries is zero
- setToList-∈: opaque bridge from list membership to set membership

New module Certs.Properties.ApplyWithdrawalsPoV:
- applyOne-pov: single withdrawal step decreases getCoin by amt
- foldl-applyOne-pov: fold induction with Unique invariant
- applyWithdrawals-pov: top-level lemma for PRE-CERT-pov
- ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves
  domain membership for other credentials

Remaining assumptions (deferred to agda-sets library):
- ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys
- sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ'
- setToList-Unique: credential uniqueness of withdrawal list
- ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming

Add preservation-of-value property modules for the Dijkstra era,
adapted from the Conway PoV proof structure for CIP-159 (partial
withdrawals and direct deposits).

New modules:
- Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov,
  PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics)
- Certs.Properties.PoV: CERTS-pov top-level theorem
- Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing
  applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls
- Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement
  with proof sketch for direct deposit cancellation

Design notes:
- PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction)
  instead of Conway's constMap/res-decomp/sumConstZero chain
- LEDGER-pov identifies the applyDirectDeposits cancellation as the
  main new proof obligation vs Conway
- applyWithdrawals-pov is structured as three layers: single-step
  (applyOne-pov), fold induction (foldl-applyOne-pov), top-level

Status: Skeleton with holes; does not yet fully typecheck.

There were unresolved proof obligations from Conway.