proposition: Lemma discrete_stable_plus : forall A (c : nat -> U) (p : nat -> A), stable_plus (discrete c p).
proof: Proof. red; intros. repeat rewrite discrete_simpl. apply Oeq_trans with (serie (fun k : nat => c k * f (p k) + c k * g (p k))). apply serie_eq_compat. intros; unfold fplus. apply Udistr_plus_left. apply (H (p k)). apply serie_plus; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)