proposition: Lemma serie_prod_le : forall (f g : nat -> U) (c:U), (forall k, f k <= c) -> wretract g -> serie (fun k => f k * g k) <= c * serie g.
proof: Proof. intros; apply Ole_trans with (serie (fun k => c * g k)); auto. Qed.
imports: ALEA(Utheory)