proposition: Lemma aeW {d} {T : semiRingOfSetsType d} {R : realFieldType} (mu : {measure set _ -> \bar R}) (P : T -> Prop) : (forall x, P x) -> {ae mu, forall x, P x}.
proof: Proof. move=> aP; have -> : P = setT by rewrite predeqE => t; split. by apply/negligibleP; [rewrite setCT|rewrite setCT measure0]. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)