proposition: Lemma cover_let : forall (A B:Type)(m1: distr A)(m2: A->distr B) (P:set A)(cP:MF A)(f:MF B)(p:U), cover P cP -> 1 <= mu m1 cP -> (forall x:A, P x -> p <= mu (m2 x) f) -> p <= mu (Mlet m1 m2) f.
proof: Proof. intros A B m1 m2. simpl; unfold star; intuition. apply Ole_trans with (mu m1 (fun x => p * (cP x))). rewrite (mu_stable_mult m1 p cP). apply Ole_trans with (p * 1); auto. apply (mu_monotonic m1). intro x. apply (cover_elim (P:=P) (f:=cP) H x); auto; intros (Hp,cPeq). rewrite cPeq; repeat Usimpl; auto. rewrite cPeq; repeat Usimpl; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)