have : k ≃ n := Rel.symm (Rel.trans ‹n ≃ 0 + k› zero_add)
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
⊢ Positive n
case mpr
ℕ : Type
inst✝³ : Core ℕ
inst✝² : Induction ℕ
inst✝¹ : Addition ℕ
inst✝ : Sign ℕ
order_inst : Order ℕ
n : ℕ
x✝ : 0 < n
k : ℕ
left✝ : Positive k
right✝ : n ≃ 0 + k
this : k ≃ n
⊢ Positive n