have diff_expand
    {w x y z : ℤ} : (w-x) * (y-z) ≃ (w*y + x*z) - (x*y + w*z)
    := by
  let wy := w*y; let wz := w*z; let xy := x*y; let xz := x*z
  calc
    _ = (w-x) * (y-z)           := rfl
    _ ≃ w * (y-z) - x * (y-z)   := AA.distribR
    _ ≃ (wy - wz) - x * (y-z)   := AA.substL AA.distribL
    _ ≃ (wy - wz) - (xy - xz)   := AA.substR AA.distribL
    _ ≃ (wy - wz) + -(xy - xz)  := Integer.sub_defn
    _ ≃ (wy - wz) + (xz - xy)   := AA.substR Integer.sub_neg_flip
    _ ≃ (wy + -wz) + (xz - xy)  := AA.substL Integer.sub_defn
    _ ≃ (wy + -wz) + (xz + -xy) := AA.substR Integer.sub_defn
    _ ≃ (wy + xz) + (-wz + -xy) := AA.expr_xxfxxff_lr_swap_rl
    _ ≃ (wy + xz) + (-xy + -wz) := AA.substR AA.comm
    _ ≃ (wy + xz) + -(xy + wz)  := AA.substR (Rel.symm Integer.neg_compat_add)
    _ ≃ (wy + xz) - (xy + wz)   := Rel.symm Integer.sub_defn
ℕ ℤ : 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 : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
⊢ (p ^ a) ^ b ≃ p ^ (a * 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 : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
k j : ℕ
b_eqv : b ≃ Coe.coe k - Coe.coe j
pow_expand : (p ^ a) ^ b ≃ (p ^ n) ^ k / (p ^ m) ^ k / ((p ^ n) ^ j / (p ^ m) ^ j)
pow_combine : ∀ {w x y z : ℕ}, (p ^ w) ^ x * (p ^ y) ^ z ≃ p ^ (w * x + y * z)
multi_compat : ∀ {w x y z : ℕ}, Coe.coe (w * x + y * z) ≃ Coe.coe w * Coe.coe x + Coe.coe y * Coe.coe z
diff_expand : ∀ {w x y z : ℤ}, (w - x) * (y - z) ≃ w * y + x * z - (x * y + w * z)
⊢ (p ^ a) ^ b ≃ p ^ (a * b)