proposition: Lemma random_stable_plus : forall n, stable_plus (random n).
proof: Proof. unfold stable_plus, fplus; intros. repeat (rewrite random_simpl). unfold fplusok, finv in H. apply Oeq_trans with (sigma (fun k : nat => ([1/]1+n * f k) + ([1/]1+n * g k)) (S n)). apply sigma_eq_compat; intros. assert (f k <= [1-] (g k)); auto. apply sigma_plus with (f:=fun k : nat => Unth n * f k) (g:=fun k : nat => Unth n * g k); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)