mathlib3

8db96a8f - feat(combinatorics/double_counting): Double-counting the edges of a bipartite graph (#11372)

feat(combinatorics/double_counting): Double-counting the edges of a bipartite graph (#11372) This proves a classic of double-counting arguments: If each element of the `|α|` elements on the left is connected to at least `m` elements on the right and each of the `|β|` elements on the right is connected to at most `n` elements on the left, then `|α| * m ≤ |β| * n` because the LHS is less than the number of edges which is less than the RHS. This is put in a new file `combinatorics.double_counting` with the idea that we could gather double counting arguments here, much as is done with `combinatorics.pigeonhole`.