proposition: Lemma dlet_dunit_id mu : \dlet_(t <- mu) (dunit t) =1 mu.
proof: Proof. move=> x; rewrite dletE (psum_finseq (r := [:: x])) //. move=> y; rewrite !inE dunit1E mulf_eq0 pnatr_eq0. by case/norP; rewrite eqb0 negbK. by rewrite big_seq1 dunit1E eqxx mulr1 ger0_norm. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum