intro (p : ℚ) (_ : AP (p ≄ 0))
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
⊢ on_diff_pow n₁ m₁ ≃ on_diff_pow n₂ m₂
ℕ ℤ : Type
inst✝¹⁰ : Natural ℕ
inst✝⁹ : Integer ℤ
inst✝⁸ : Integer.Induction ℤ
ℚ : Type
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Sign ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
n₁ m₁ n₂ m₂ : ℕ
x✝¹ : Coe.coe n₁ - Coe.coe m₁ ≃ Coe.coe n₂ - Coe.coe m₂
p : ℚ
x✝ : AP (p ≄ 0)
⊢ on_diff_pow n₁ m₁ p ≃ on_diff_pow n₂ m₂ p