have : sgn (p + q) ≃ s := calc
  sgn (p + q)
    ≃ _ := sgn_subst (add_substL ‹p ≃ a/b›)
  sgn ((a : ℚ)/b + q)
    ≃ _ := sgn_subst (add_substR ‹q ≃ c/d›)
  sgn ((a : ℚ)/b + (c : ℚ)/d)
    ≃ _ := sgn_subst add_div_integers
  sgn (((a * d + b * c : ℤ) : ℚ)/((b * d : ℤ) : ℚ))
    ≃ _ := sgn_div_integers
  sgn (a * d + b * c) * sgn (b * d)
    ≃ _ := Rel.symm Integer.sgn_compat_mul
  sgn ((a * d + b * c) * (b * d))
    ≃ _ := Integer.sgn_subst AA.distribR
  sgn (a * d * (b * d) + b * c * (b * d))
    ≃ _ := Integer.sgn_subst (AA.substL AA.expr_xxfxxff_lr_swap_rl)
  sgn (a * b * (d * d) + b * c * (b * d))
    ≃ _ := Integer.sgn_subst (AA.substR AA.expr_xxfxxff_lr_swap_rl)
  sgn (a * b * (d * d) + b * b * (c * d))
    ≃ _ := Integer.add_preserves_sign sgn_abdd sgn_bbcd
  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
this : sgn (c * d) ≃ s
sgn_abdd : sgn (a * b * (d * d)) ≃ s
sgn_bbcd : sgn (b * b * (c * d)) ≃ 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_abdd : sgn (a * b * (d * d)) ≃ s
sgn_bbcd : sgn (b * b * (c * d)) ≃ s
this : sgn (p + q) ≃ s
⊢ sgn (p + q) ≃ s