proposition: Lemma serie_mult : forall (f : nat -> U) c, wretract f -> serie (fun k => c * f k) == c * serie f.
proof: Proof. unfold serie; intros. apply Oeq_trans with (lub (UMult c @ sigma f)); auto. apply lub_eq_compat; apply fmon_eq_intro; intro n. apply (sigma_mult (f:=f) c (n:=n)); auto. Qed.
imports: ALEA(Utheory)