`BookProof.QgOuterFockInteractionFL.nextPart_ne` {n : ℕ} (hn : 2 ≤ n) (p : Fin n) (hp : p.val = 0) : nextPart p ≠ p

Initializing...

`BookProof.QgOuterFockInteractionFL.nextPart_ne` {n : ℕ} (hn : 2 ≤ n) (p : Fin n) (hp : p.val = 0) : nextPart p ≠ p · Prove2Me