fact: Definition dlim_bump (mu : nat -> {distr T / R}) : dlim (fun n => mu n.+1) =1 dlim mu.
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum