have : sgn x ≃ 1 := calc
  sgn x                   ≃ _ := Rational.sgn_subst ‹x ≃ a / b›
  sgn ((a : ℚ) / (b : ℚ)) ≃ _ := Rational.sgn_div_integers
  sgn a * sgn b           ≃ _ := ‹sgn a * sgn b ≃ 1›
  1                       ≃ _ := Rel.refl
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁷ : AP (Positive a)
this✝⁶ : sgn a ≃ 1
this✝⁵ : AP (Positive b)
this✝⁴ : sgn b ≃ 1
this✝³ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝² : sgn a ≃ sgn b
this✝¹ : Nonzero b
this✝ : Integer.Sqrt1 (sgn b)
this : sgn a * sgn b ≃ 1
⊢ Positive x
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
x✝ : AltPositive x
a b : ℤ
a_pos : AP (Positive a)
b_pos : AP (Positive b)
x_eqv : x ≃ Rational.from_integer a / Rational.from_integer b
this✝⁸ : AP (Positive a)
this✝⁷ : sgn a ≃ 1
this✝⁶ : AP (Positive b)
this✝⁵ : sgn b ≃ 1
this✝⁴ : x ≃ Rational.from_integer a / Rational.from_integer b
this✝³ : sgn a ≃ sgn b
this✝² : Nonzero b
this✝¹ : Integer.Sqrt1 (sgn b)
this✝ : sgn a * sgn b ≃ 1
this : sgn x ≃ 1
⊢ Positive x