proposition: Lemma cover_esp_mult_right : forall (A:Type)(P:set A)(p:U)(f:MF A), cover P f -> forall x, p & f x == p * f x.
proof: Proof. intros; apply Uesp_zero_one_mult_right. exact (cover_orc_0_1 H x). Qed.
imports: ALEA(Utheory) ALEA(Sets)