proposition: Lemma SDistr_rightneutral : forall A : ord_choiceType, SDistr_bind A A (SDistr_unit A) = Id (SDistr_carrier A).
proof: Proof. intro A. simpl. eapply boolp.funext. unfold "=1". intro de. apply distr_ext. apply dlet_dunit_id. Qed.
imports: Coq(Relation_Definitions Morphisms) mathcomp(all_ssreflect all_algebra distr reals realsum) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd Axioms)