multiplicity a b returns the largest natural number n such that a ^ n ∣ b, as an enat or natural with infinity. If ∀ n, a ^ n ∣ b, then it returns ⊤