unfold Nat.ModEq at h2
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 % c = d ^ (a - n) % c
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) % c