exact 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
this✝² : Integer.Sqrt1 (sgn b)
this✝¹ : sgn a * sgn b ≃ 1
this✝ : sgn x ≃ 1
this : Positive x
⊢ Positive x
no goals