no goals
a b : ℕ
hab : coprime a b
⊢ _root_.Disjoint (factorization a).support (factorization b).support
simpa only [support_factorization] using
  disjoint_toFinset_iff_disjoint.mpr (coprime_factors_disjoint hab)