∀ {α : Type u_1} [inst : Ring α]
  (motive :
    (x x_1 : α) →
      (x_2 x_3 : ℤ) →
        (x_4 x_5 : ℕ) →
          Mathlib.Meta.NormNum.IsRat x x_2 x_4 →
            Mathlib.Meta.NormNum.IsRat x_1 x_3 x_5 →
              decide (x_2.mul (Int.ofNat x_5) ≤ x_3.mul (Int.ofNat x_4)) = true → Prop)
  (x x_1 : α) (x_2 x_3 : ℤ) (x_4 x_5 : ℕ) (x_6 : Mathlib.Meta.NormNum.IsRat x x_2 x_4)
  (x_7 : Mathlib.Meta.NormNum.IsRat x_1 x_3 x_5)
  (x_8 : decide (x_2.mul (Int.ofNat x_5) ≤ x_3.mul (Int.ofNat x_4)) = true),
  (∀ (num num_1 : ℤ) (da db : ℕ) (inv : Invertible ↑da) (inv_1 : Invertible ↑db)
      (h : decide (num.mul (Int.ofNat db) ≤ num_1.mul (Int.ofNat da)) = true),
      motive (↑num * ⅟↑da) (↑num_1 * ⅟↑db) num num_1 da db ⋯ ⋯ h) →
    motive x x_1 x_2 x_3 x_4 x_5 x_6 x_7 x_8