have : n ≥ step 0 := AA.substLFn literal_step ‹n ≥ 1›
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
⊢ Positive n
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : n ≥ 1
this : n ≥ step 0
⊢ Positive n