(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949)

(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949)

This PR introduces a new arithmetic kind for indexed root predicates.
An indexed root predicate compares a real variable to the k'th root of a given polynomial as follows:
Let IRP_k(x ~ 0, p) an indexed root predicate with k a non-negative number, x some real variable, ~ an arithmetic relation (e.g. =, <, ...), and p a polynomial over x (and possibly other variables).
If p contains variables apart from x, we can only evaluate the expression over a suitable assignment for at least these variables.
The evaluation of this expression is equivalent to computing the k'th real root of p in x (with all other variables evaluated over a given assignment) and comparing this real root to zero (according to the relation symbol ~).

Note that we currently do not intend to use this structure for solving, but require it for representing and printing CAD proofs.