apply H a n b c d h1.symm h2 han
case inr
n a b c d : ℕ
h1 : n ≡ a [MOD b]
h2 : d ^ b ≡ 1 [MOD c]
H : ∀ (n a b c d : ℕ), n ≡ a [MOD b] → d ^ b ≡ 1 [MOD c] → n ≤ a → d ^ n ≡ d ^ a [MOD c]
h : ¬n ≤ a
han : a ≤ n
⊢ d ^ a ≡ d ^ n [MOD c]
no goals