You can convert homogeneous rational equations in side lengths (such as $a^2 + b^2 = c^2$) into equivalent Tarski-geometric statements. In particular, convert it to a rational equation of degree 1 (e.g. $a^2/c + b^2/c = c$), construct each of the monomial terms using repeated application of the Intersecting Chords Theorem, and sum the terms on each side of the equation by concatenating lengths.