rw [mul_comm, pow_mul, Nat.pow_mod, h2, ←Nat.pow_mod, one_pow]
case h₁
n a b c d : ℕ
h2 : d ^ b % c = 1 % c
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 % c = d ^ ((a - n) / b * b) % c
no goals