proposition: Lemma im_distr_id : forall A (f:A->A) (m:Distr A), (forall x, f x = x) -> im_distr f m == m.
proof: Proof. intros; apply eq_distr_intro; simpl; intros. apply (mu_stable_eq m); simpl; apply ford_eq_intro; intro x; rewrite H; auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)