proposition: Lemma Mdiv_stable_inv : forall A (k:U) (d:distr A)(dk : mu d (fone A) <= k), stable_inv (Mdiv k (mu d)).
proof: Proof. red; intros; repeat rewrite Mdiv_simpl. apply (Ueq_orc 0 k); auto; intros. repeat (rewrite Udiv_by_zero;auto). assert (forall f, mu d f <= k). intros; apply Ole_trans with (mu d (fone A)); auto. apply Ole_trans with ((mu d (fone A) - mu d f) / k); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)