have : AP (Positive (-a)) := AP.mk ‹Positive (-a)›
ℚ : 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)
⊢ AltPositive x
ℚ : 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))
⊢ AltPositive x