have : Integer.Sqrt1 (sgn b) := Integer.sgn_nonzero.mp this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁵ : AP (Positive a)
this✝⁴ : sgn a ≃ 1
this✝³ : AP (Positive b)
this✝² : sgn b ≃ 1
this✝¹ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝ : sgn a ≃ sgn b
this : Nonzero b
⊢ Positive x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁶ : AP (Positive a)
this✝⁵ : sgn a ≃ 1
this✝⁴ : AP (Positive b)
this✝³ : sgn b ≃ 1
this✝² : x ≃ Rational.from_integer a / Rational.from_integer b
this✝¹ : sgn a ≃ sgn b
this✝ : Nonzero b
this : Integer.Sqrt1 (sgn b)
⊢ Positive x