In my opinion, current area of circle proof shouldn't be moved to the main part yet, but not only because it's a "fruit of the poison tree", but also since of the ongoing formalization of measure theory in
set.mm. As far as I understand, Glauco Siliprandi's mathbox already contains the formalization of the n-dimensional Lebesgue measure on RR ^m X, as well as theorems about volumes of n-dimensional cubes, etc. It seems that this is more or less enough to reduce the computation of the area to essentially the same integral which was computed in areacirc.
As for the other results, like Heine-Cantor theorem and especially Brouwer fixed point theorem for the unit cube, they certainly deserve being moved to the main part. Since there are no sections in your mathbox, these theorems do not appear in the table of contents and remain a bit obscure. Half-angle theorems probably can be moved to the section "The exponential, sine and cosine functions" of "Elementary trigonometry"; there's already a group of statements about addition/subtraction formulae for trigonometric functions.