have : sgn a * sgn b ≃ 1 := calc
  sgn a * sgn b     ≃ _ := Rel.symm Rational.sgn_div_integers
  sgn ((a : ℚ) / b) ≃ _ := Rational.sgn_subst (Rel.symm ‹x ≃ a / b›)
  sgn x             ≃ _ := Rational.sgn_positive.mp ‹Positive x›
  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
⊢ 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
⊢ AltPositive x