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.