proposition: Lemma duni1E s x : (duni s) x = (x \in s)%:R / (size (undup s))%:R.
proof: Proof. by unlock duni; rewrite drat1E count_uniq_mem ?(mem_undup, undup_uniq). Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum