`BookProof.SmBrstGhost.ghostNumber_comm_ghostAnn` (m : ℕ) (a : Fin 12) : ghostNumber m * ghostAnn m a - ghostAnn m a * ghostNumber m = -ghostAnn m a

Initializing...

`BookProof.SmBrstGhost.ghostNumber_comm_ghostAnn` (m : ℕ) (a : Fin 12) : ghostNumber m * ghostAnn m a - ghostAnn m a * ghostNumber m = -ghostAnn m a · Prove2Me