`BookProof.ChapterParityQL.QLParity_order_four` : QLParity * QLParity ≠ 1 ∧ QLParity * QLParity * (QLParity * QLParity) = 1

Initializing...

`BookProof.ChapterParityQL.QLParity_order_four` : QLParity * QLParity ≠ 1 ∧ QLParity * QLParity * (QLParity * QLParity) = 1 · Prove2Me