proposition: Lemma mcond_stable_inv : forall A (m:distr A) (f: MF A), stable_inv (mcond (mu m) f).
proof: Proof. red; intros. repeat rewrite mcond_simpl. apply (Ueq_orc 0 (mu m f)); intro. auto. rewrite (Udiv_by_zero (mu m (fconj f (finv f0))) (y:=mu m f)); auto. apply Ole_trans with (mu m (fminus f (fconj f f0)) / mu m f). apply Udiv_le_compat_left. apply (mu_monotonic m). intro x; unfold fconj,finv,fminus; auto. rewrite stable_minus_distr; trivial. rewrite Udiv_minus; trivial. Qed.
imports: ALEA(Utheory) ALEA(Sets)