no goals
n d a : Int
a0 : a ≠ 0
⊢ a * n /. (a * d) = n /. d
if d0 : d = 0 then simp [d0] else
simp [divInt_eq_iff (Int.mul_ne_zero a0 d0) d0, Int.mul_assoc, Int.mul_left_comm]
no goals
n d a : Int
a0 : a ≠ 0
d0 : d = 0
⊢ a * n /. (a * d) = n /. d
simp [d0]
no goals
n d a : Int
a0 : a ≠ 0
d0 : ¬d = 0
⊢ a * n /. (a * d) = n /. d
simp [divInt_eq_iff (Int.mul_ne_zero a0 d0) d0, Int.mul_assoc, Int.mul_left_comm]