have : x ≃ ((-a : ℤ) : ℚ) / ((-b : ℤ) : ℚ) := calc
  x                               ≃ _ := ‹x ≃ a / b›
  (a : ℚ) / b                     ≃ _ := Rel.symm Rational.div_neg_cancel
  (-(a : ℚ)) / (-(b : ℚ))         ≃ _ := Rational.div_substL neg_eqv
  ((-a : ℤ) : ℚ) / (-b : ℚ)       ≃ _ := Rational.div_substR neg_eqv
  ((-a : ℤ) : ℚ) / ((-b : ℤ) : ℚ) ≃ _ := Rational.eqv_refl
ℚ : 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
ℚ : 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