(L : List BandRecord) {m : ℕ} (hm : L.length - 1 ≤ m) : ledgerHi L m - ledgerLo L m = ledgerHi L (L.length - 1) - ledgerLo L (L.length - 1)

-- Generated from ChapterSirkBandLedger.lean — theorem BookProof.SirkBandLedger.ledger_width_eventually_const
import Mathlib
import Definitions.Def_ChapterSirkBandLedger
open BookProof.SirkBandLedger















open BookProof.SirkCertificateReader
open BookProof.BandEnclosure

theorem BookProof.SirkBandLedger.ledger_width_eventually_const (L : List BandRecord) {m : ℕ}
    (hm : L.length - 1 ≤ m) :
    ledgerHi L m - ledgerLo L m
      = ledgerHi L (L.length - 1) - ledgerLo L (L.length - 1) := by sorry