`int_ideal_cofactors : term list -> term -> term list`

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

DESCRIPTION
The call int_ideal_cofactors [`p1`; ...; `pn`] `p`, where all the terms have type :int 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 INT_RING or a slight elaboration of INT_POLY_CONV, for example)
```  p = p1 * q1 + ... + pn * qn
```
hence providing an explicit certificate for the ideal membership. If ideal membership does not hold, int_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. At present this is a generic version for fields, and in rare cases it may fail because cofactors are found involving non-trivial rational numbers even where there are integer cofactors. This imperfection should be fixed eventually, and is not usually a problem in practice.

EXAMPLE
In the case of a singleton list, ideal membership just amounts to polynomial divisibility, e.g.
```  # prioritize_int();;
val it : unit = ()

# int_ideal_cofactors
[`r * x * (&1 - x) - x`]
`r * (r * x * (&1 - x)) * (&1 - r * x * (&1 - x)) - x`;;
[`&1 * r pow 2 * x pow 2 +
-- &1 * r pow 2 * x +
-- &1 * r * x +
&1 * r +
&1`]
```

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