no goals
α : Type u_1
inst✝¹ : Monoid α
inst✝ : DecidableRel fun x x_1 => x ∣ x_1
a b : α
m : ℕ
h : Finite a b
hm : Part.get (multiplicity a b) h < m
⊢ multiplicity a b < ↑m
rwa [← PartENat.coe_lt_coe, PartENat.natCast_get] at hm