Zmod simple proofs

Stream: new members

[Renaud Lifchitz]

Hello,

I would like to prove the simple following lemma:

lemma congr_squared (n a b : ℕ) : a ≡ b [ZMOD n] → a^2 ≡ b^2 [ZMOD n]

but I'm always struggling with types/casts problems... Can somebody show me the right way to do it?

Thanks.

[Alex J. Best]

There are two different ways of working with $\mathbf Z/n\mathbf Z$ in mathlib: one is using a ≡ b [ZMOD n], which is just a notation for  a % n = b %n (% is remainder upon division), but the terms a, b are still nats, as this is just a random relation one cannot necessarily rewrite the terms in the same way you would with an equality.
The other way is the using the type zmod n which is the type $\mathbf Z/n\mathbf Z$, so if you set it up like this it should work

lemma congr_squared (n a b : ℕ) : (a : zmod n) = b  → (a : zmod n)^2 = (b : zmod n)^2 :=
begin
intro h,
rw h,
end

[Alex J. Best]

One way of doing your original formulation is using the similar lemma int.modeq.modeq_mul

lemma congr_squared (n a b : ℕ) : a ≡ b [ZMOD n] → a^2 ≡ b^2 [ZMOD n]
:= begin
  intro h,
  rw pow_two,
  rw pow_two,
  exact int.modeq.modeq_mul h h,
end

[Renaud Lifchitz]

Great, I understand, that was confusing, thank you!