simp only [Nat.zero_mod, add_zero]
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 + 0 % b) % 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) / b * b) % c