∀ {num : ℤ} {den g : ℕ} (dvd_num : ↑g ∣ num) (dvd_den : g ∣ den) (den_nz : den / g ≠ 0)
  (reduced : (num / ↑g).natAbs.Coprime (den / g)),
  ↑g ∣ num → g ∣ den → Rat.maybeNormalize num den g dvd_num dvd_den den_nz reduced = Rat.normalize num den ⋯