  We provide elementary proofs of Lemmas 7.1 and 7.4 appearing in "The
Cartan-Hadamard conjecture and the Little Prince", by B. Kloeckner and G.
Kuperberg. The Lemmas play an important role in the derivation of novel
isoperimetric inequalities. The original proofs relied on Sage, a symbolic
algebra package, to factor certain algebraic varieties into irreducible
components.
