case inl
α : Type u
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n

case inr
α : Type u
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
α : Type u
x y n : ℕ
⊢ x - y ∣ x ^ n - y ^ n
cases' le_or_lt y x with h h
case inl
α : Type u
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n
case inl
α : Type u
x y n : ℕ
h : y ≤ x
⊢ x - y ∣ x ^ n - y ^ n
have : y ^ n ≤ x ^ n := Nat.pow_le_pow_of_le_left h _
no goals
case inl
α : Type u
x y n : ℕ
h : y ≤ x
this : y ^ n ≤ x ^ n
⊢ x - y ∣ x ^ n - y ^ n
exact_mod_cast sub_dvd_pow_sub_pow (x : ℤ) (↑y) n
case inr
α : Type u
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n
case inr
α : Type u
x y n : ℕ
h : x < y
⊢ x - y ∣ x ^ n - y ^ n
have : x ^ n ≤ y ^ n := Nat.pow_le_pow_of_le_left h.le _
no goals
case inr
α : Type u
x y n : ℕ
h : x < y
this : x ^ n ≤ y ^ n
⊢ x - y ∣ x ^ n - y ^ n
exact (Nat.sub_eq_zero_of_le this).symm ▸ dvd_zero (x - y)