have : sgn (-a) ≃ 1 := calc
  sgn (-a)   ≃ _ := Integer.sgn_compat_neg
  (-(sgn a)) ≃ _ := AA.subst₁ ‹sgn a ≃ sgn b›
  (-(sgn b)) ≃ _ := Rel.symm Integer.sgn_compat_neg
  sgn (-b)   ≃ _ := ‹sgn (-b) ≃ 1›
  1          ≃ _ := Rel.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
⊢ 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
⊢ AltPositive x