have ann : a = (a - n + n) := by exact (Nat.sub_eq_iff_eq_add h).mp rfl
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
⊢ 1 * d ^ n ≡ d ^ a [MOD c]
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
h : n ≤ a
ann : a = a - n + n
⊢ 1 * d ^ n ≡ d ^ a [MOD c]