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