proposition: Lemma mcond_stable_mult : forall A (m:distr A) (f: MF A), stable_mult (mcond (mu m) f).
proof: Proof. red; intros. repeat rewrite mcond_simpl. rewrite <- Umult_div_assoc. apply Udiv_eq_compat_left. apply Oeq_trans with (mu m (fmult k (fconj f f0))). apply (mu_stable_eq m). simpl; apply ford_eq_intro; unfold fconj, fmult; intro; auto. apply (mu_stable_mult m). apply (mu_monotonic m); auto. apply fle_fconj_left. Qed.
imports: ALEA(Utheory) ALEA(Sets)