have : p^(step n') > q^(step n') := calc
  _ ≃ p^(step n') := eqv_refl
  _ ≃ p           := pow_step_zero
  _ > q           := ‹p > q›
  _ ≃ q^(step n') := eqv_symm pow_step_zero
ℕ ℤ : 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
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 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
n' : ℕ
ih : n' > 0 → p ^ n' > q ^ n' ∧ q ^ n' ≥ 0
x✝ : step n' > 0
this✝ : n' ≃ 0 ∨ n' > 0
h✝ : n' ≃ 0
pow_step_zero : ∀ {x : ℚ}, x ^ step n' ≃ x
this : p ^ step n' > q ^ step n'
⊢ p ^ step n' > q ^ step n' ∧ q ^ step n' ≥ 0