case mpr =>
  intro (_ : n ≥ 1)
  show Positive n
  have : n ≥ step 0 := AA.substLFn literal_step ‹n ≥ 1›
  have : n > 0 := lt_step_le.mpr this
  have : Positive n := lt_zero_pos.mpr this
  exact this
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
⊢ n ≥ 1 → Positive n
no goals