feat(combinatorics/configuration): Points and lines inequality (#10772)
feat(combinatorics/configuration): Points and lines inequality (#10772)

If a nondegenerate configuration has a unique line through any two points, then there are at least as many lines as points.





leanprover-community/mathlib,leanprover-community/mathlib