DivideExact​(AngouriMath.​Functions.​MultivariatePolynomial)

The leading term in lexicographic order is cancelled at each step, which lowers
it strictly, so the loop terminates; when the divisor really divides, its
leading term divides the leading term of what is left every time, and what
remains at the end is zero. Anything else — a leading term that will not divide,
or a remainder that never reaches zero — is the answer that it does not divide.
That is the check the caller relies on: nothing is cancelled that has not been
divided out and seen to leave nothing behind.