proposition: Lemma mu_one_inv : forall (A : Type)(m:distr A), mu m (fone A) == 1 -> forall f, mu m (finv f) == [1-] (mu m f).
proof: Proof. intros; apply Ole_antisym. apply (mu_stable_inv m f). apply Uplus_le_simpl_left with (mu m f); auto. setoid_rewrite (Uinv_opp_right (mu m f)). apply Ole_trans with (mu m (fun x => (f x) + [1-] (f x))). setoid_rewrite <- H; apply (mu_monotonic m); auto. assert (H1 : fplusok f (finv f)). red; unfold finv; intro x; auto. setoid_rewrite <- (mu_stable_plus m H1); auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)