proposition: Lemma mcond_stable_plus : forall A (m:distr A) (f: MF A), stable_plus (mcond (mu m) f).
proof: Proof. red; intros. repeat rewrite mcond_simpl. simpl; rewrite <- Udiv_plus. apply Udiv_eq_compat_left. assert (fplusok (fconj f f0) (fconj f g)). auto. rewrite <- (mu_stable_plus m H0). apply (mu_stable_eq m). simpl; apply ford_eq_intro; intro x; unfold fconj,fplus; auto. apply Udistr_plus_left; auto. apply (H x). Qed.
imports: ALEA(Utheory) ALEA(Sets)