proposition: Lemma cover_esp_fun_le : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U), (forall x, P x -> f x <= g x) -> cover P cP -> forall x, cP x & f x <= cP x & g x.
proof: Proof. intros. apply (cover_elim H0 x); auto; intuition. rewrite H3; repeat Usimpl; auto. rewrite H3; repeat Usimpl; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)