no goals
m✝ n a b c d m : ℕ
h : a ≡ b [MOD n]
⊢ a ^ m ≡ b ^ m [MOD n]
induction m with
| zero => rfl
| succ d hd =>
  rw[pow_succ, pow_succ]
  exact hd.mul h
no goals
case zero
m n a b c d : ℕ
h : a ≡ b [MOD n]
⊢ a ^ zero ≡ b ^ zero [MOD n]
rfl
case succ
m n a b c d✝ : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]
case succ
m n a b c d✝ : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ succ d ≡ b ^ succ d [MOD n]
rw[pow_succ, pow_succ]
no goals
case succ
m n a b c d✝ : ℕ
h : a ≡ b [MOD n]
d : ℕ
hd : a ^ d ≡ b ^ d [MOD n]
⊢ a ^ d * a ≡ b ^ d * b [MOD n]
exact hd.mul h