# Reduce not handling 0 == a properly

Consider

Reduce[a == 0 \[Implies] a == 0]
Reduce[a == 0 \[Implies] 0 == a]
Reduce[a == 0 ∧ b == 0 \[Implies] a == 0 ∧ b == 0]
Reduce[a == 0 ∧ b == 0 \[Implies] a == 0 ∧ 0 == b]
Reduce[a == 0 ∧ b == 0 \[Implies] 0 == a ∧ 0 == b]


The first four predictably produce True, but the last gives

(b == 0 && a == 0) || a != 0 || b != 0


which is: a) incorrect, and b) why all of a sudden?

### Edit

My questions remain. However, in the meantime I have been looking for workarounds. I started with looking for patterns like: Equal[a_, (b_Symbol | b_Subscript)], with the intent to switch around a and b, then ToRules[], etc.

However, I stumbled upon LogicalExpand[] which does the switcheroo by itself:

Reduce[a == 0 ∧ b == 0 \[Implies] LogicalExpand[0 == a ∧ 0 == b]]


producing the desired True.

For your last expression, you can use Simplify[]:
Reduce[a == 0 ∧ b == 0 \[Implies] 0 == a ∧ 0 == b] // Simplify

which returns True as expected. This kind of situation happens for algebraic expressions also. Sometimes you need Expand[], Factor[], or even FullSimplify[] to produce a True for an equation. There may be other ways, specific to logical expressions, such as LogicalExpand[] which do similar kinds of transformations.
The problem arises because Mathematica only uses a limited number of automatic simplifications. For example (x + y) + (z - x) == y = z returns True while (x - y)(x + y) == x^2 - y^2 returns unchanged unless Expand or Simplify or Factor is applied before it also returns True.