# Use `positive` in `gmultiset` representation to avoid off-by-one computations.

- The only lemma where the use of internal use
`nat`

appeared was`gmultiset_subseteq_alt`

, but that lemma talks about`gmultiset_car`

, which should be private. I thus flagged that lemma as`Local`

. - This change also gives rise to more compact representations (that is logarithmic instead of linear in terms of the largest multiplicity), but since the multiplicity and scalar_mult functions (as part of the public API) use
`nat`

, it's difficult to come up with an example where this improvement can be observed.