change (a * (x % b)) % b = c % b
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) ≡ c [MOD b]
case h.right
a b c : ℕ
hb : 0 < b
h : a.Coprime b
N : ℕ
HN1 : N ≡ 0 [MOD a]
x : ℕ
hx : N = a * x
HN2 : N % b = c % b
⊢ a * (x % b) % b = c % b