∀ (motive : ℚ → Prop) (h : ℚ),
  (∀ (num : ℤ) (den : ℕ) (den_nz : den ≠ 0) (reduced : num.natAbs.Coprime den),
      motive { num := num, den := den, den_nz := den_nz, reduced := reduced }) →
    motive h