`real_ideal_cofactors : term list -> term -> term list`

SYNOPSIS
Produces cofactors proving that one real polynomial is in the ideal generated by others.

DESCRIPTION
The call real_ideal_cofactors [`p1`; ...; `pn`] `p`, where all the terms have type :real and can be considered as polynomials, will test whether p is in the ideal generated by the p1,...,pn. If so, it will return a corresponding list [`q1`; ...; `qn`] of `cofactors' such that the following is an algebraic identity (provable by REAL_RING or a slight elaboration of REAL_POLY_CONV, for example):
```  p = p1 * q1 + ... + pn * qn
```
hence providing an explicit certificate for the ideal membership. If ideal membership does not hold, real_ideal_cofactors fails. The test is performed using a Gr\"obner basis procedure.

FAILURE CONDITIONS
Fails if the terms are ill-typed, or if ideal membership fails.

EXAMPLE
Here is a fairly simple example:
``` # prioritize_real();;
val it : unit = ()

# real_ideal_cofactors
[`y1 * y3 + x1 * x3`;
`y3 * (y2 - y3) + (x2 - x3) * x3`]
`x3 * y3 * (y1 * (x2 - x3) - x1 * (y2 - y3))`;;
...
val it : term list = [`&1 * y3 pow 2 + -- &1 * y2 * y3`; `&1 * y1 * y3`]
```
and we can confirm the identity as follows (note that REAL_IDEAL_CONV already does this directly):
```  # REAL_RING `(&1 * y3 pow 2 + -- &1 * y2 * y3) * (y1 * y3 + x1 * x3) +
(&1 * y1 * y3) * (y3 * (y2 - y3) + (x2 - x3) * x3) =
x3 * y3 * (y1 * (x2 - x3) - x1 * (y2 - y3))`;;
```

When we say that terms can be `considered as polynomials', we mean that initial normalization, essentially in the style of REAL_POLY_CONV, will be applied, but some complex constructs such as conditional expressions will be treated as atomic.