have neg_eqv {z : ℤ} : -(z : ℚ) ≃ ((-z : ℤ) : ℚ) :=
  Rational.eqv_symm Rational.neg_compat_from_integer
ℚ : 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))
⊢ 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))
this : AP (Positive (-b))
neg_eqv : ∀ {z : ℤ}, -Rational.from_integer z ≃ Rational.from_integer (-z)
⊢ AltPositive x