have : sgn (c * d) ≃ s := calc
  sgn (c * d)     ≃ _ := Integer.sgn_compat_mul
  sgn c * sgn d   ≃ _ := Rel.symm sgn_div_integers
  sgn ((c : ℚ)/d) ≃ _ := sgn_subst (eqv_symm ‹q ≃ c/d›)
  sgn q           ≃ _ := ‹sgn q ≃ s›
  s               ≃ _ := Rel.refl
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝³ : p ≃ from_integer a / from_integer b
this✝² : q ≃ from_integer c / from_integer d
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : Integer.Sqrt1 (sgn d)
this : sgn (a * b) ≃ s
⊢ sgn (p + q) ≃ s
ℕ ℤ ℚ : Type
inst✝⁹ : Natural ℕ
inst✝⁸ : Integer ℤ
inst✝⁷ : Core ℚ
inst✝⁶ : Addition ℚ
inst✝⁵ : Multiplication ℚ
inst✝⁴ : Negation ℚ
inst✝³ : Subtraction ℚ
inst✝² : Reciprocation ℚ
inst✝¹ : Division ℚ
inst✝ : Sign ℚ
s : ℤ
p q : ℚ
x✝¹ : sgn p ≃ s
x✝ : sgn q ≃ s
a b : ℤ
b_nonzero✝¹ : Integer.Nonzero b
p_eqv : p ≃ from_integer a / from_integer b
c d : ℤ
b_nonzero✝ : Integer.Nonzero d
q_eqv : q ≃ from_integer c / from_integer d
this✝⁴ : p ≃ from_integer a / from_integer b
this✝³ : q ≃ from_integer c / from_integer d
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : Integer.Sqrt1 (sgn d)
this✝ : sgn (a * b) ≃ s
this : sgn (c * d) ≃ s
⊢ sgn (p + q) ≃ s