I am looking for a development defining finite support (sub)-probability distribution on an arbitrary type (in particular without decidable equality).

Is there any up to date library for doing proof about this kind of basic probability theory in Coq ? I am aware of ALEA but it seems rather outdated (Coq 8.3).