Expected codeword length is at least entropy

For any finite type $\iota$ with a Fintype instance, a function $p:\iota\to\mathbb{R}$, and a natural number $D$, the auxiliary definition entropy p D is $-\sum_{i\in\iota} p_i\cdot\log_D(p_i)$, where $\log_D(x)$ is Real.logb D x, itself defined as $\dfrac{\log x}{\log D}$ using the natural logarithm and with $D$ coerced from $\mathbb{N}$ to $\mathbb{R}$ (no positivity or $D\neq 1$ hypothesis is built into this definition itself); separately, for a type $\alpha$ and a set $S\subseteq \mathrm{List}\,\alpha$ of finite lists over $\alpha$, UniquelyDecodable S unfolds to: for every pair of finite lists of lists $L_1,L_2 : \mathrm{List}(\mathrm{List}\,\alpha)$ — i.e. every finite ordered sequence of "words" over $\alpha$, of any length, with repetitions allowed — such that every word occurring in $L_1$ lies in $S$ and every word occurring in $L_2$ lies in $S$, if the concatenation (flatten) of all the words of $L_1$ in order equals the concatenation of all the words of $L_2$ in order (as a single list over $\alpha$), then $L_1=L_2$ as lists outright — same length, same words, in the same order (not merely the same multiset of words). The theorem expected_length_ge_entropy then fixes: a plain (universe-0) type $\iota$ with Fintype and Nonempty instances (the "source symbols"); a function $p:\iota\to\mathbb{R}$ together with the hypothesis hp_pos that $p_i>0$ strictly for every single $i\in\iota$ with no exceptions, and the hypothesis hp_sum that $\sum_{i\in\iota}p_i=1$ exactly (so $p$ is a probability distribution on $\iota$ with full support — every symbol has strictly positive probability, none can be zero); a plain type $\alpha$ with Fintype and Nonempty instances (the "code alphabet") together with the hypothesis hD that $\mathrm{card}(\alpha)\ge 2$ (an alphabet of size at least two, redundant with but not derived from the separate Nonempty α instance); a function $c:\iota\to\mathrm{List}\,\alpha$ assigning to each symbol a finite string over the alphabet, together with hinj, that $c$ is injective (distinct symbols get distinct codewords); and hc, that the set $\mathrm{range}(c)=\{c(i):i\in\iota\}\subseteq \mathrm{List}\,\alpha$ is uniquely decodable in the exact sense unfolded above. Under all these hypotheses simultaneously, the conclusion is the single inequality $-\sum_{i\in\iota} p_i\cdot\log_{\mathrm{card}(\alpha)}(p_i)\ \le\ \sum_{i\in\iota} p_i\cdot |c(i)|$, where the left side is entropy p (Fintype.card α) fully unfolded (base-$|\alpha|$ logarithmic entropy of $p$, with $|\alpha|=\mathrm{card}(\alpha)$ cast to $\mathbb{R}$), and the right side is the expectation under $p$ of $|c(i)|$, the length of the codeword list $c(i)$ (a natural number, coerced to $\mathbb{R}$ for the multiplication); the inequality is non-strict ($\le$), and both sums range over the full index set $\iota$ with no restriction or partial sum anywhere in the statement.