rfl
case h₂
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ d ^ n ≡ d ^ n [MOD c]

case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]
case h₁
n a b c d : ℕ
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
h1 : 0 ≡ a - n [MOD b]
⊢ 1 ≡ d ^ (a - n) [MOD c]