∀ {α : Type u_1} [inst : Semiring α]
  (motive :
    (x x_1 : α) →
      (x_2 x_3 x_4 x_5 : ℕ) →
        Mathlib.Meta.NormNum.IsNNRat x x_2 x_4 →
          Mathlib.Meta.NormNum.IsNNRat x_1 x_3 x_5 → decide (x_2 * x_5 < x_3 * x_4) = true → Prop)
  (x x_1 : α) (x_2 x_3 x_4 x_5 : ℕ) (x_6 : Mathlib.Meta.NormNum.IsNNRat x x_2 x_4)
  (x_7 : Mathlib.Meta.NormNum.IsNNRat x_1 x_3 x_5) (x_8 : decide (x_2 * x_5 < x_3 * x_4) = true),
  (∀ (num num_1 da db : ℕ) (inv : Invertible ↑da) (inv_1 : Invertible ↑db) (h : decide (num * db < num_1 * 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