Add applyWithdrawals-pov and applyDirectDeposits-pov

Step 3 of the LEDGER preservation-of-value plan (#1187).

These two lemmas describe the value flow through the per-transaction
withdrawal and direct-deposit handling that bracket the inner CERTS
step inside the new ENTITIES rule (#1201):

+  applyWithdrawals-pov: getCoin rwds ≡ getCoin (applyWithdrawals w r) + getCoin w
+  applyDirectDeposits-pov: getCoin (applyDirectDeposits d r) ≡ getCoin r + getCoin d

Both are proved by induction over setToList of the underlying
RewardAddress ⇀ Coin map, with a per-step lemma about applyOne (the
lambda body of applyToRewards) at each inductive step.

The withdrawal version requires the per-batch NetworkId witness and a
Unique-on-stake-projection invariant on the remaining fold list,
because truncating subtraction (_∸_) means an already-reduced balance
must never be revisited.  The direct-deposit version drops both --
addition is total and commutative, so a re-visit is harmless -- and
the resulting signature is correspondingly leaner.

The module ApplyToRewards-PoV is parameterised over three set/map
identities to be discharged in a follow-up:

+  ∪ˡ-lookup-preserve
+  sum-map-proj₂≡getCoin
+  setToList-Unique  (used only by applyWithdrawals-pov)

File location reflects the post-#1201 home of applyWithdrawals and
applyDirectDeposits: Entities.Specification.<...>, not
Certs.Specification.<...>.

Author: williamdemeo