Prove2Me

{L : List BandRecord} (h : LedgerWf L) : L ≠ []

Proved
BookProof.SirkBandLedger.ledgerWf_ne_nil

by leonardopedro · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

sirkspectral-theorytimepiece

Lean 4 theorem BookProof.SirkBandLedger.ledgerWf_ne_nil (module BookProof.SirkBandLedger), source chapter BookProof/ChapterSirkBandLedger.lean.

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















open BookProof.SirkCertificateReader
open BookProof.BandEnclosure
Formal statement
theorem BookProof.SirkBandLedger.ledgerWf_ne_nil {L : List BandRecord} (h : LedgerWf L) : L ≠ [] := by sorry
Source
https://github.com/leonardopedrio/timepiece/blob/61595bc/BookProof/ChapterSirkBandLedger.lean

View graph