Rank inequality for cocompact discontinuous groups

Let $G/H$ be a homogeneous space in the reductive setting, and let $K$ be a maximal compact subgroup of $G$. Rank inequality conjecture. If $G/H$ admits a cocompact discontinuous group, then

$$\operatorname{rank}G+\operatorname{rank}(H\cap K)\geq\operatorname{rank}H+\operatorname{rank}K.$$

This is an obstruction to cocompact discontinuous groups for homogeneous spaces with non-compact $H$. The source says that the inequality was proved by Kobayashi--Ono in the equal-rank case and later in general by Morita and Tholozan, so the conjecture is solved.