proposition: Lemma mu_inv_minus_inv : forall (A:Type) (m:distr A)(f: MF A), mu m (finv f) + [1-](mu m (fone A)) == [1-](mu m f).
proof: Proof. intros; apply Uminus_eq_perm_right. apply Uinv_le_compat. apply (mu_monotonic m); unfold fone; auto. unfold Uminus. rewrite mu_inv_minus; repeat Usimpl. unfold Uminus. apply Uinv_eq_compat; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)