Let $n>2$ and assume that a binary linear code of length $n$ has MAXIMUM distance $D\leq (n+1)/2$. Assume that all coordinates of the code are essential in the sense that some codeword is 1 there.
Then $D=(n+1)/2= 2^k$ for some $k\geq 1$, and the code is equivalent to the punctured Hadamard code with parameters $[2^{k+1}-1, k+1, 2^k]_2$.
I managed to prove this, and deduced an interesting statement about finite permutation groups. I couldn't find either of the two results in the literature.
Question: Is the above statement known? If yes, could you give me a reference, please?