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