case step =>
  intro (n' : ℕ) (And.intro (_ : p^n' ≥ q^n') (_ : q^n' ≥ 0))
  show p^(step n') ≥ q^(step n') ∧ q^(step n') ≥ 0
  have : p ≥ 0 := ge_trans ‹p ≥ q› ‹q ≥ 0›
  have : p^(step n') ≥ q^(step n') := calc
    _ ≃ p^(step n') := eqv_refl
    _ ≃ p^n' * p    := pow_step
    _ ≥ q^n' * p    := le_substL_mul_nonneg ‹p ≥ 0› ‹p^n' ≥ q^n'›
    _ ≥ q^n' * q    := le_substR_mul_nonneg ‹q^n' ≥ 0› ‹p ≥ q›
    _ ≃ q^(step n') := eqv_symm pow_step
  have : q^(step n') ≥ 0 := calc
    _ ≃ q^(step n') := eqv_refl
    _ ≃ q^n' * q    := pow_step
    _ ≥ 0 * q       := le_substL_mul_nonneg ‹q ≥ 0› ‹q^n' ≥ 0›
    _ ≃ 0           := mul_absorbL
  exact And.intro ‹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
⊢ ∀ (m : ℕ), p ^ m ≥ q ^ m ∧ q ^ m ≥ 0 → p ^ step m ≥ q ^ step m ∧ q ^ step m ≥ 0
no goals