Prove that $H<GRightarrow |H|le leftlfloor frac{|G|}{2}rightrfloor$ without Lagrange's theorem.

Suppose we do not have yet the notion of coset, and thence Lagrange’s theorem either. So, if $G$ is a finite group and $H<G$, we just know that $H$ is a nonempty, proper, closed subset of $G$.

(How) Can we prove, in this framework, that $|H|le leftlfloor frac{|G|}{2} rightrfloor$?

Some facts we might be using are, e.g. (here $f$ denotes group’s operation):

• $f(Htimes H) = H$
• $f(Htimes (Gsetminus H))= Gsetminus H$

Based on this, I’ve tried to come up with some equation/inequality involving the cardinalities of the "level sets" $L_a^{H×H}:={(h,h’)∈H×Hmid hh’=a}$ for $a∈H$, and $L_a^{H×H^c}:={(h,c)∈H×H^cmid hc=a}$ for $a∈H^c$ (where $H^c:=Gsetminus H$), but unsuccessfully.

---

Addendum. Some more stuff, just to see whether the idea may get to somewhere. We have:

begin{alignat}{1}
|H|^2 &= sum_{ain H}|L_a^{Htimes H}| \
&= |H|+sum_{ain Hsetminus{e}}|L_a^{Htimes H}| \
end{alignat}

whence:

begin{alignat}{1}
|H|cdot(|H|-1) &= sum_{ain Hsetminus{e}}|L_a^{Htimes H}| \
tag 1
end{alignat}

Moreover:

begin{alignat}{1}
|H||H^c| &= sum_{ain H^c}|L_a^{Htimes H^c}| \
tag 2
end{alignat}

By $(1)$ and $(2)$, we get both:

begin{alignat}{1}
|H|cdot(|G|-1) &= sum_{ain H^c}|L_a^{Htimes H^c}| + sum_{ain Hsetminus{e}}|L_a^{Htimes H}| \
tag 3
end{alignat}

and:

begin{alignat}{1}
|H|cdot(|H^c|-|H|+1) &= sum_{ain H^c}|L_a^{Htimes H^c}| – sum_{ain Hsetminus{e}}|L_a^{Htimes H}| \
tag 4
end{alignat}

If from $(3)$ and/or $(4)$ we could deduce that $|H|mid |G|$ (or, equivalently, $|H|mid |H^c|$), we’d get actually more than what I originally asked, namely a "coset-free" proof of Lagrange’s theorem.