have : a * b - a * c ≃ 0 := zero_diff_iff_eqv.mpr ‹a * b ≃ a * c›
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
⊢ b ≃ c
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
inst✝ : Subtraction ℤ
a b c : ℤ
x✝¹ : a ≄ 0
x✝ : a * b ≃ a * c
this : a * b - a * c ≃ 0
⊢ b ≃ c