proposition: Lemma cover_union : forall (A:Type)(P Q:set A)(f g : MF A), cover P f -> cover Q g -> cover (union P Q) (fplus f g).
proof: Proof. unfold cover; intros. case (H x); case (H0 x); unfold union,fplus; split; intros. case H5; intro. apply Ole_trans with (f x); auto. apply Ole_trans with (g x); auto. assert (~P x); try tauto. assert (~Q x); try tauto. apply Ole_trans with (0+0); auto. apply Uplus_le_compat; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)