real_ideal_cofactors : term list -> term -> term list
p = p1 * q1 + ... + pn * qn
# 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`]
# 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))`;;