have : p^(0:ℕ) ≥ q^(0:ℕ) := calc
  _ ≃ p^0 := eqv_refl
  _ ≃ 1   := pow_zero
  _ ≃ q^0 := eqv_symm pow_zero
  _ ≥ q^0 := le_refl
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
⊢ p ^ 0 ≥ q ^ 0 ∧ q ^ 0 ≥ 0
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Subtraction ℚ
inst✝⁵ : Reciprocation ℚ
inst✝⁴ : Division ℚ
inst✝³ : Sign ℚ
inst✝² : Order ℚ
inst✝¹ : Metric ℚ
inst✝ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
p q : ℚ
n : ℕ
left✝ : p ≥ q
right✝ : q ≥ 0
this : p ^ 0 ≥ q ^ 0
⊢ p ^ 0 ≥ q ^ 0 ∧ q ^ 0 ≥ 0