proposition: Lemma cover_eq_zero_elim : forall (A:Type)(P:set A)(f:MF A) (z:A), cover P f -> f z == 0 -> ~ P z.
proof: Proof. intros; apply (excluded_middle (A:=P z)); intros; auto. case Udiff_0_1. rewrite <- H0. apply (cover_eq_one (P:=P) (f:=f)); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)