proposition: Lemma P_deltaE (A B : Type) (f : {hom A, B}) : P_delta # f = P_delta_left # f :> (_ -> _).
proof: Proof. exact: funext. 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