∀ {α : Type u_1} [inst : DivisionSemiring α]
  (motive : (x x_1 : α) → (x_2 x_3 : ℕ) → Mathlib.Meta.NormNum.IsNNRat (x * x_1⁻¹) x_2 x_3 → Prop) (x x_1 : α)
  (x_2 x_3 : ℕ) (x_4 : Mathlib.Meta.NormNum.IsNNRat (x * x_1⁻¹) x_2 x_3),
  (∀ (x x_5 : α) (x_6 x_7 : ℕ) (h : Mathlib.Meta.NormNum.IsNNRat (x * x_5⁻¹) x_6 x_7), motive x x_5 x_6 x_7 h) →
    motive x x_1 x_2 x_3 x_4