proposition: Lemma random_stable_mult : forall n, stable_mult (random n).
proof: Proof. unfold stable_mult, fmult; intros; repeat (rewrite random_simpl). apply Oeq_trans with (sigma (fun l : nat => k * ([1/]1+n * f l)) (S n)). apply sigma_eq_compat; intros; auto. apply sigma_mult with (f:=fun k : nat => Unth n * f k). red; intros. apply Ole_trans with ([1/]1+n); auto. apply Ole_trans with ([1-] (sigma (fun k1 => Unth n) k0)); auto. apply (@fnth_retract n k0); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)