theorem proved decidable or rfl

`arithmetic_before_time`

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

formal statement (Lean)

  97theorem arithmetic_before_time :
  98    Before Stage.arithmeticObject Stage.timeTick := by

Decided by rfl or decide.

  99  decide
 100

Lean names referenced from this declaration's body.