proposition: Lemma fdistbind1 (R: realType) A (p : fdist R A) : p >>= @fdist1 R A = p.
proof: Proof. apply/fdist_ext => /= a; rewrite fdistbindE /= (bigD1 a) //= fdist1xx mulr1. by rewrite big1 ?addr0// => a0 a0a; rewrite fdist10 ?mulr0// eq_sym. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR logb realType_ext ssr_ext ssralg_ext bigop_ext