Improve `Ledger.Core.Specification.Epoch`

[carlostome]

The "bisimulation" property proved in #941 requires two extra assumptions on the Epoch type:

e<sucᵉ : ∀ {e : Epoch} → e < sucᵉ e
≤-predᵉ : ∀ {e e' : Epoch} → sucᵉ e ≤ sucᵉ e' → e ≤ e'

These are rather ad-hoc since the relations < and ≤ on Epoch are derived from that on the type Slot while sucᵉ is primitive to Epoch.

In addition, it seems that:

1. Epoch has a least element and this is implicitly assumed to correspond to the Epoch of the zeroth slot epoch 0#.
2. The semiring structure on Slot ought to interact with the partial order defined on it (monotonicity of binary operations e.g.,) , however these structures are totally independent atm.
3. The semiring structure assumed on Slot comes with its own notion of equality but in the rest this is unused and "replaced" by decidable propositional equality.

I think it would be a good idea to refactor this module in such a way that:

1. Epoch has its own partial order.
2. Epoch has a least element.
3. The Epoch partial order interacts well with sucᵉ.
4. The partial orders on Slot and Epoch are related via firstSlot and epoch (both functions are monotone). Maybe even epoch 0# = 0 and firstSlot 0 = 0#.