@acer 

    The goal is to be able to use symbolic math, where the result analyzes properly for:

m * x <= m * y

where x <= y

    Using a "-5" for "m," the result fails an "is" block "-5 * x <= -5 *y", yet succeeds for "-5 (x <= y)".

    However, when attempting to place m back into the question that works, there is a syntax error: "m*(x<=y)."

    Using map doesn't resolve the issue either.

Sam

P.S. I'm unsure what you mean by toy; I simplified this to help communicate the issue.

study_symbolic_inequalities.mw

@acer

   I tried the use of map to get around the distributed/associativity issue.  It really doesnt help.  The flow of the conversation started with me using -5, but really its a series of symbols on my end, and this is a simplification with the issue.  The root, the value of the 'm', can be negative leading to the need to invert the inequality as @Carl Love pointed out.  We all can see the inequality needs to be inverted, and that the 'is' shows it's not.  

    Oddly, I've come across this converting from MathCad to Maple, where the terminology to define the assumption somehow in MathCad yields the ability to solve symbolically.  I'm new to Maple, so trying to find the art to do the same in Maple.  Even more odd, is I did quick check on other symbolic math engines, and they all suffer on inequialities.  Not that I intend to go back to MathCad - I just intend to learn how to get the symbolic solver in Maple to understand that M * (x<=y) is true for all M, even when M is negative. 

@Carl Love 

   I am using Maple mostly for symbolic math, and not for any true result.  I went to try the distributed '-5' symbolically, and ran right into another problem.  The 1st "is" shoud be false and is.  The 2nd "is" is to show the distributed symbolic math equivalent of the '-5'; which errors.  The 3rd 'is' is a simplier form, and works, albeit not against the 'y' variable but some contrived value to just see where the issue is with distributed operations on inequalities.

... any hoo.... work-around doesn't work, so I'll have to contrive an alternative.

restart;
assume(m < 0, x <= y, 0 < x);
is(m*x <= m*y);
                             false

is(m(x <= y));
Error, (in is) invalid input: m(x <= y)
is(m*x <= 0);
                              true

:) ... to make matters worse.... the assumption knows when there's a blatant contradiction, just not with inequalities and negative coeficients.

assume(x <= y, -5*x <= x, -5*y <= y, -5*x <= -5*y);
is(-5*x <= -5*y);
                              true

assume(x <= y, -5*x <= x, -5*y <= y, -5*x <= -5*y, -5*(x <= y));
is(-5*x <= -5*y);
                              true

assume(x <= y, -5*x <= x, -5*y <= y, -5*x <= -5*y, -5*(x <= y), y < x);
Error, (in assume) contradictory assumptions

@Carl Love 

   Yep (you are right, math wise), I guess I am expecting something different from the symbolic solver.  My thinking is since I am asking Maple to solve symbolically, that it would understand the -5 on each side of the inequality placed manually by me, would do the the inversion of the inequiality.  When Maple knows the -5 is being distributed it knows to invert the inequality.  When I invert the inequality Maple symbolically gets the right answer.  So, IDK, mathematically the first "-5*x <= -5*y" where the assumption tells Maple -5 applied to the variable inverts the inequality.  

I'll chalk this up to me being extra lazy, and when using symbolic math I'll need to adjust the inequalities or use distribution. 

ok... (I modified, the < should have been a <= for the last is)

restart;
assume(x <= y, -5*x <= x, -5*y <= y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                              true

is(-5*y <= -5*x);
                              true

I give :), symbolic math :) .. I have to do the inequality inversion if I don't distribute the -5.

restart;
assume(x <= y, -5*x <= x, -5*y <= y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                              true

@Carl Love 

    yeh, restart is helping this at least be consistent.  Albeit, I simply do not understand how the two "is" blocks are mathematically different.  

restart;
assume(x <= y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                              true

restart;
assume(x <= y, 0 <= x, 0 <= y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                              true

restart;
assume(x <= y, -1*x < x, -1*y < y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                              true

@Carl Love

   to even further complicate, by explicity telling Maple the - * inequality inverses the inequiality, I get the same result as not having that in the assumption.  Really confusing.

assume(x <= y, -1*x < x, -1*y < y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                              true

@Carl Love 

huh, I'm going to have to think about this.  There is something about what you've pointed out, just it's not intuitive to me.  I altered the assumption, and then both are false.  With the original assumption, they differ, yet mathematically the two "is" blocks are the same (leading to my confusion).

assume(x <= y, 0 <= x, 0 <= y);
is(-5*x <= -5*y);
                             false

is(-5*(x <= y));
                             false

@Carl Love 

   well, ah, wouldn't both "is" blocks produce the same result?  
   I think what you are saying, is that the distribution of the -5 happens after the "is" block is done.  I guess I am still confused.  Nm used a math operation, yet I had the "is" block with the math operation within the paranthesis.   Presumably, the distribution of "-5" would complete before the "is" block finishes.

@Carl Love 

  yeh, maybe... 

@nm

  well, at least I'm not the only one thinking this is a bug.  I'm so new to Maple I was wondering if I had some syntax issue.

  Thank you,