proposition: Lemma cover_inter_mult : forall (A:Type)(P Q:set A)(f g : MF A), cover P f -> cover Q g -> cover (inter P Q) (fun x => f x * g x).
proof: Proof. unfold cover; intros. case (H x); case (H0 x); unfold inter; split; intros. case H5; intros. apply Ole_trans with (1*1); auto. apply Umult_le_compat; auto. assert (orc (~ P x) (~ Q x)); auto. apply orc_intro; tauto. apply H6; auto; intro. apply Ole_trans with (f x); auto. apply Ole_trans with (g x); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)