have : k ≄ 0 := AA.inject ‹coe k ≄ coe (0 : ℕ)›
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝¹ : a - b ≃ coe k
this✝ : a - b ≄ 0
this : coe k ≄ 0
⊢ Positive (a - b)
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
x✝ : b < a
left✝ : b ≤ a
right✝ : b ≄ a
k : ℕ
h✝ : a ≃ b + coe k
this✝² : a - b ≃ coe k
this✝¹ : a - b ≄ 0
this✝ : coe k ≄ 0
this : k ≄ 0
⊢ Positive (a - b)