Consider the following sage code:
a,b,c = var('a b c')
simplify(a + b == a + c)
I would expect the result of this code to be b == c, but sage gives me a + b == a + c. The only way to actually simplify the equation is to use add_to_both_sides(-a). For more complicated equations this seems to be hardly applicable. Why doesn't simplify() (or full_simplify()) take care of this properly?
