exact AltPositive.mk this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : Positive x
a b : Integer.Impl.Difference ℕ
b_nonzero✝ : Nonzero b
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : sgn a * sgn b ≃ 1
left✝ : Integer.Sqrt1 (sgn b)
right✝ : sgn a ≃ sgn b
this✝⁶ : sgn b ≃ 1 ∨ sgn b ≃ -1
h✝ : sgn b ≃ -1
this✝⁵ : sgn (-b) ≃ 1
this✝⁴ : sgn (-a) ≃ 1
this✝³ : Positive (-a)
this✝² : Positive (-b)
this✝¹ : AP (Positive (-a))
this✝ : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
this : x ≃ Rational.from_integer (-a) / Rational.from_integer (-b)
⊢ AltPositive x
no goals