ring with natural number division

Stream: general

[Chris Hughes]

Is ring supposed to solve this goal? The n / 2 should be treated as atoms right?

example (n : ℕ) : (n / 2) + (n / 2) = 2 * (n / 2) := by ring --fails

[Kenny Lau]

but N isn't a ring

[Chris Hughes]

ring is supposed to work with commutative semirings I believe.

[Mario Carneiro]

#1557