proposition: Lemma serie_inv_le : forall (f g : nat -> U), wretract f -> serie (fun k => f k * [1-] (g k)) <= [1-] (serie (fun k => f k * g k)).
proof: Proof. unfold serie; intros. apply lub_lub_inv_le; intros. rewrite sigma_inv; auto. Qed.
imports: ALEA(Utheory)