show c * b ≃ a * d
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c//d ≃ a//b
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b c d : ℤ
x✝ : a//b ≃ c//d
this : a * d ≃ c * b
⊢ c * b ≃ a * d