proposition: Lemma mcond_continuous : forall A (m:distr A) (f: MF A), continuous (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 (lub (c:=A -O-> U) h))) (y:=mu m f)); auto. apply Umult_div_le_right. apply Ole_trans with (mu m (lub (c:=A -O-> U) ((Fconj A f)@h))). apply mu_monotonic. apply (continuous2_app (F:=Fconj A) (fconj_continuous2 (A:=A)) f h). rewrite (mu_continuous m). rewrite <- (lub_comp_le (UMult <_> (mu m f)) (mcond (mu m) f @ h) ). apply (lub_le_compat (D:=U)). intro x; simpl. rewrite Udiv_mult; auto. apply (mu_monotonic m); auto. apply fle_fconj_left. Qed.
imports: ALEA(Utheory) ALEA(Sets)