Neighbourhood bound for a square-free bipartite graph (source code)

= Neighbourhood bound for a square-free bipartite graph

Let $A$ be $k$ vertices of a bipartite graph, each of degree at least $k$. If the graph has no $4$-cycle, then $|N(A)|\geq2k-1$. Indeed, any pair in $A$ has at most one common neighbour, so
$$
\sum_{y\in N(A)}\binom{d_A(y)}2\leq\binom k2.
$$
If $|N(A)|\leq2k-2$, Cauchy--Schwarz and $\sum_y d_A(y)\geq k^2$ make the left side strictly larger than $\binom k2$, a contradiction.