[Dijkstra] Gov PoV: GOVS-coinFromGovDeposit and rmOrphanDRepVotes-coinFromGovDeposit (Gov.Properties.PoV)

# Description

**Parent issue**: #1123 (umbrella). **Context**: PR #1203 (`LEDGER-pov`, #1187).

`LEDGER-pov` accounts for governance-action deposits via `coinFromGovDeposit : GovState → Coin` (the sum of `GovActionState.deposit`, added in PR #1203) and takes two facts about it as module parameters (`src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md`, provenance comments inline), to be proved in a new `Gov.Properties.PoV` module:

1. `GOVS-coinFromGovDeposit` — a `GOVS` step grows `coinFromGovDeposit` by exactly `govProposalsDeposits` of the step's proposals. Provenance: `GOV-Propose` stores `deposit = pp .govActionDeposit`, and no `GOV-Vote` (or in-`LEDGER` removal) changes a stored deposit.

2. `rmOrphanDRepVotes-coinFromGovDeposit` — `rmOrphanDRepVotes` only rewrites `votes.gvDRep`, never `GovActionState.deposit`, so it leaves `coinFromGovDeposit` unchanged.

These are consumed by `SUBLEDGERS-gov-coin` (the per-sub-transaction `GOVS` steps) and `gov-acc` (the top-level `GOVS` step) in the `LEDGER-V` equational chain.

## Acceptance criteria

- [ ] A new module `Ledger.Dijkstra.Specification.Gov.Properties.PoV` proves both lemmas, green under `--safe`.
- [ ] Statements match the `LEDGER-PoV` module parameters verbatim, so the eventual rewiring of `Ledger.Properties.PoV` can consume them directly.