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