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