proposition: Lemma dmargin_dunit (t : T) (f : T -> U): dmargin f (dunit t) =1 dunit (f t) :> {distr U / R}.
proof: Proof. by apply/dlet_unit. Qed.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum