have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp ‹Integer.Nonzero b›
ℕ ℤ ℚ : 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
⊢ 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)
⊢ sgn (p + q) ≃ s