proposition: Lemma range_cover : forall A (P:A -> Prop) d cP, range P d -> cover P cP -> forall f, mu d f == mu d (fun x => cP x * f x).
proof: Proof. intros; apply range_eq with (P:=P); auto; intros. rewrite (cover_eq_one a H0); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)