proposition: Lemma cover_eq_one_elim_class : forall (A:Type)(P Q:set A)(f:MF A), cover P f -> forall z, f z == 1 -> class (Q z) -> incl P Q -> Q z.
proof: Proof. intros; apply (excluded_middle (A:=P z)); intros; auto. case Udiff_0_1. rewrite <- H0. apply Oeq_sym; apply (cover_eq_zero (P:=P) (f:=f)); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)