proposition: Lemma range_eq : forall A (P:A->Prop) (d:Distr A), range P d -> forall f g, (forall a, P a -> f a == g a) -> mu d f == mu d g.
proof: Proof. red; intros; apply Ole_antisym; apply (range_le (P:=P)); intros; auto. apply Oeq_le; apply Oeq_sym; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)