tactic for doing calculation with mod

Stream: new members

[Patrick Lutz]

Is there a tactic (or some other way I guess) to take care of calculations in modular arithmetic? E.g. something that would easily prove the following

import data.nat.basic

example (a b c : ℕ) (ha : a % 5 = 1) (hb : b % 5 = 3)
    (hc : c % 5 = 4) : (a^2 + (b + 2*c)^3) % 5 = 2 := sorry

Right now I can prove this with a series of rewrites and then a call to ring, but it seems too involved. Is there a better way?

[Chris Hughes]

I would avoid the use of % and use the type zmod for most things like this.

[Jalex Stark]

import tactic

import data.nat.basic
import data.zmod.basic

example (a b c : zmod 5) (ha : a = 1) (hb : b = 3)
  (hc : c = 4) : (a^2 + (b + 2*c)^3) = 2 :=
begin
  rw [ha, hb, hc], ring,
end