{α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [NormalizationMonoid α] →
        [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) → NormalizedGCDMonoid α