Assumption fails unless common factor is extracted

[zeehio]

Thanks for working on this great package. I believe I have found a bug, and I have a workaround but I am not familiar with the sympy codebase, so maybe this reproducible example can be useful for someone to fix it:

This reproducible example has been tested with the current git master (as well as versions 1.1.1 and 0.7.6) leading to the same results (albeit different speeds, current version being slower).

Given a, b, c with a-b > 0 and c > 0, we know (a-b)*c > 0.
However the expression a*c - b*c > 0 is not resolved to True.
As a workaround I can simplify the expression before asking. Is this a bug?

from sympy.abc import a,b,c
from sympy.assumptions import assuming, Q, ask
from sympy import simplify

with assuming(Q.positive(a-b), Q.positive(c)):
    # This works:
    print("Should be True and it is:", ask(Q.positive((a-b)*c))) # True!
    # Expand the product: (a-b)*c = a*c - b*c
    # Now this fails:
    print("Should be True and it is:", ask(Q.positive(a*c - b*c))) # None :-(
    # Workaround: Simplify the expansion
    print("Should be True and it is:", ask(Q.positive(simplify(a*c - b*c)))) # True

[smichr]

factor_terms is a good function to use for this purpose instead of the more general simplify.

[asmeurer]

Assumptions on expressions are still in the infant stage. Generally speaking, assuming that a complicated expression is positive won't get you very far unless that expression appears exactly in your expression. By complicated expression, I mean anything other than a symbol. For symbols, just set the assumption on the symbol (Symbol('a', positive=True)). These per-symbol assumptions work very well, and are beyond the infant stage.

[asmeurer]

By the way, another workaround is to let x = a - b, and replace a with x + b. That way, you can use the old assumptions on single symbols.

>>> a, b = symbols('a b')
>>> x, c = symbols('x c', positive=True)
>>> expr = a*c - b*c
>>> expr.subs(a, x + b).expand().is_positive
True