proposition: Lemma mu_zero : forall (A : Type)(m : distr A), mu m (fzero A) == 0.
proof: Proof. intros. apply Oeq_trans with (mu m (fmult 0 (fzero A))); auto. apply mu_stable_eq; unfold fmult; simpl; auto. apply Oeq_trans with (0 * (mu m (fzero A))); auto. apply mu_stable_mult; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)