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