Entropy of a distribution is nonnegative

For all $\htmlData{mx=1}{\iota \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{p : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$, if $\htmlData{mx=4}{\forall i,\ 0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{p}(\htmlData{mx=1}{i})}}$ and $\htmlData{mx=4}{\forall i,\ \htmlData{mx=2}{\htmlData{mx=0}{p}(\htmlData{mx=1}{i})} \mathrel{\htmlData{mx=3}{\leq}} 1}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\iota}}$), then