have swap_middle : (p * p⁻¹) * (q * q⁻¹) ≃ (p * q) * (p⁻¹ * q⁻¹) :=
  AA.expr_xxfxxff_lr_swap_rl
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Subtraction ℚ
inst✝⁴ : Reciprocation ℚ
inst✝³ : Division ℚ
inst✝² : Sign ℚ
p q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
inv_p : 1 ≃ p * p⁻¹
inv_q : 1 ≃ q * q⁻¹
swap_middle : p * p⁻¹ * (q * q⁻¹) ≃ p * q * (p⁻¹ * q⁻¹)
⊢ (p * q)⁻¹ ≃ p⁻¹ * q⁻¹