feat(combinatorics/configuration): The order of a projective plane is at least 2 (#11550)
feat(combinatorics/configuration): The order of a projective plane is at least 2 (#11550)

This PR proves that the order of a projective plane is strictly larger than 1.





leanprover-community/mathlib,leanprover-community/mathlib