proposition: Lemma cover_ok : forall (A:Type)(P Q:set A)(f g : MF A), (forall x, P x -> ~ Q x) -> cover P f -> cover Q g -> fplusok f g.
proof: Proof. red; red; intros. intro x; unfold finv. apply (cover_elim H0 x); auto; intuition. rewrite H4; auto. apply (cover_elim H1 x); auto; intuition. rewrite H6; auto. case (H x H3 H5). Qed.
imports: ALEA(Utheory) ALEA(Sets)