proposition: Lemma gcm_retE (T : Type) (x : choice_of_Type T) : Ret x = necset1 (fsdist1 x) :> gcm T.
proof: Proof. rewrite /= /ret_ /Monad_of_category_monad.ret /=. rewrite !HCompId !HIdComp /=. rewrite /id_f /= /etaC. unlock => /=. by rewrite eta0E eta1E. Qed.
imports: Reals mathcomp(all_ssreflect) mathcomp(boolp classical_sets) mathcomp(finmap) infotheo(Reals_ext classical_sets_ext ssrR ssr_ext) infotheo(fdist fsdist convex necset) monae_lib HB(structures) category hierarchy