A tactic for simplifying identities in not-necessarily-commutative rings.
An example:
example {R : Type*} [ring R] (a b c : R) : a * (b + c + c - b) = 2*a*c :=
by noncomm_ring
tactic.noncomm_ring
A tactic for simplifying identities in not-necessarily-commutative rings.
An example:
example {R : Type*} [ring R] (a b c : R) : a * (b + c + c - b) = 2*a*c :=
by noncomm_ring