noncomm_ring tactic #
Solve goals in not necessarily commutative rings.
This tactic is rudimentary, but useful for solving simple goals in noncommutative rings. One
glaring flaw is that numeric powers are unfolded entirely with
pow_succ and can easily exceed the
maximum recursion depth.
noncomm_ring is just a
simp only [some lemmas] followed by
abel. It automatically uses
to close the goal, and if that doesn't succeed, defaults to