calc
  _ = p₁^a           := rfl
  _ ≃ p₁^((n:ℤ) - m) := pow_substR ‹a ≃ n - m›
  _ ≃ p₁^n / p₁^m    := pow_diff
  _ ≃ p₂^n / p₁^m    := div_substL (Natural.pow_substL ‹p₁ ≃ p₂›)
  _ ≃ p₂^n / p₂^m    := div_substR (Natural.pow_substL ‹p₁ ≃ p₂›)
  _ ≃ p₂^((n:ℤ) - m) := eqv_symm pow_diff
  _ ≃ p₂^a           := pow_substR (Rel.symm ‹a ≃ n - m›)
ℕ ℤ : 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₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ p₁ ^ a ≃ p₂ ^ a
no goals