A partition of a natural number
n is a way of writing
n as a sum of positive integers, where the
order does not matter: two sums that differ only in the order of their summands are considered the
same partition. This notion is closely related to that of a composition of
n, but in a composition
n the order does matter.
A summand of the partition is called a part.
p : partition nis a structure, made of a multiset of integers which are all positive and add up to
The main motivation for this structure and its API is to show Euler's partition theorem, and related results.
The representation of a partition as a multiset is very handy as multisets are very flexible and already have a well-developed API.
Given a multiset which sums to
n, construct a partition of
n with the same multiset, but
without the zeros.
The number of times a positive integer
i appears in the partition
of_sums n l hl is the same
as the number of times it appears in the multiset
i = 0,
partition.non_zero combined with
multiset.count_eq_zero_of_not_mem gives that