Basic algebraic operations

Stream: new members

[YH]

What's a better way to do something like 3 * m + m by 4 * m?
right now I'm doing 3 * m + m = 3 * m + 1 * m = (3+1) * m = 4 * m.

[Kevin Buzzard]

the ring tactic proves this immediately, assuming m is in a semiring.

[YH]

I tried ring already, but what I had was h : x ≤ 3 * m + m, and ring doesn't seem work for that?

[Kevin Buzzard]

then rw (show 3 * m + m = 4 * m, by ring)

[YH]

OK thanks.