proposition: Lemma Mmult_stable_inv : forall A (k:MF A) (d:distr A), stable_inv (Mmult k (mu d)).
proof: Proof. red; intros; simpl. apply Ole_trans with (mu d (finv f)); auto. apply Ole_trans with ([1-]mu d f); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)