case step =>
  intro (n' : ℕ) (ih : n' > 0 → p^n' > q^n' ∧ q^n' ≥ 0) (_ : step n' > 0)
  show p^(step n') > q^(step n') ∧ q^(step n') ≥ 0
  have : n' ≃ 0 ∨ n' > 0 := Natural.gt_split ‹step n' > 0›
  match this with
  | Or.inl (_ : n' ≃ 0) =>
    have pow_step_zero {x : ℚ} : x^(step n') ≃ x := calc
      _ ≃ x^(step n') := eqv_refl
      _ ≃ x^n' * x    := pow_step
      _ ≃ x^0 * x     := mul_substL (Natural.pow_substR ‹n' ≃ 0›)
      _ ≃ 1 * x       := mul_substL pow_zero
      _ ≃ x           := mul_identL
    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
    have : q^(step n') ≥ 0 := calc
      _ ≃ q^(step n') := eqv_refl
      _ ≃ q           := pow_step_zero
      _ ≥ 0           := ‹q ≥ 0›
    exact And.intro ‹p^(step n') > q^(step n')› ‹q^(step n') ≥ 0›
  | Or.inr (_ : n' > 0) =>
    have (And.intro (_ : p^n' > q^n') (_ : q^n' ≥ 0)) := ih ‹n' > 0›
    have : p ≥ q := ge_cases.mpr (Or.inl ‹p > q›)
    have : p > 0 := trans_gt_ge_gt ‹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    := lt_substL_mul_pos ‹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 : ℕ), (m > 0 → p ^ m > q ^ m ∧ q ^ m ≥ 0) → step m > 0 → p ^ step m > q ^ step m ∧ q ^ step m ≥ 0
no goals