lemma proved term proof

`eightbeat_holds`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  10lemma eightbeat_holds : eightbeat_prop := by

Term-mode proof.

  11  simpa using IndisputableMonolith.Patterns.period_exactly_8
  12
  13end URCAdapters
  14end IndisputableMonolith

Lean names referenced from this declaration's body.