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