calc
  (b * sgn a) * (c * sgn c) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (b * c) * (sgn a * sgn c) ≃ _ := AA.substL AA.comm
  (c * b) * (sgn a * sgn c) ≃ _ := AA.substL (Rel.symm ‹a * d ≃ c * b›)
  (a * d) * (sgn a * sgn c) ≃ _ := AA.substL AA.comm
  (d * a) * (sgn a * sgn c) ≃ _ := AA.substR AA.comm
  (d * a) * (sgn c * sgn a) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (d * sgn c) * (a * sgn a) ≃ _ := Rel.refl
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
this✝¹ : Integer.Nonzero a
this✝ : Integer.Nonzero c
this : a * d ≃ c * b
⊢ b * sgn a * (c * sgn c) ≃ d * sgn c * (a * sgn a)
no goals