True ↔ ∀ {P L : Type} (x : Membership P L) (x_1 : Fintype P) (x_2 : Fintype L) (pp : Configuration.ProjectivePlane P L), IsPrimePow (Configuration.ProjectivePlane.order P L)