have : a + b ≃ (n + k : ℕ) - (m + j : ℕ) := calc
  _ = a + b                     := rfl
  _ ≃ (n - m) + b               := AA.substL ‹a ≃ n - m›
  _ ≃ (n - m) + (k - j)         := AA.substR ‹b ≃ k - j›
  _ ≃ (n + k) - (m + j)         := Integer.sub_xchg_add
  _ ≃ (n + k : ℕ) - (m + j)     := AA.substL (Rel.symm AA.compat₂)
  _ ≃ (n + k : ℕ) - (m + j : ℕ) := AA.substR (Rel.symm AA.compat₂)
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : 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
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
⊢ p ^ (a + b) ≃ p ^ a * p ^ b
ℕ ℤ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
ℚ : 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
inst✝¹ : Exponentiation ℚ
p : ℚ
inst✝ : AP (p ≄ 0)
a b : ℤ
n m : ℕ
h✝¹ : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
h✝ : b ≃ Coe.coe k - Coe.coe j
this : a + b ≃ Coe.coe (n + k) - Coe.coe (m + j)
⊢ p ^ (a + b) ≃ p ^ a * p ^ b