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.
