calc
  sgn (a//b * c//d)       ≃ _ := sgn_subst eqv_refl
  sgn ((a * c)//(b * d))  ≃ _ := Rel.refl
  sgn (a * c)             ≃ _ := Integer.sgn_compat_mul
  sgn a * sgn c           ≃ _ := Rel.refl
  sgn (a//b) * sgn (c//d) ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ sgn (a//b * c//d) ≃ sgn (a//b) * sgn (c//d)
no goals