More aggressive `ring` tactic

Stream: general

[(deleted)]

Looks like the ring tactic shies away from cancelling out multiplication and division. I'm not sure what can be done... I'm looking for a way to assure ring that the division is nonzero so the ring tactic has every right to cancel out the division if need be...

[Aaron Liu]

sounds like field_simp