proposition: Lemma SDistr_assoc : forall (A B C : ord_choiceType) (f : TypeCat ⦅ choice_incl B; SDistr_carrier C ⦆) (g : TypeCat ⦅ choice_incl A; SDistr_carrier B ⦆), SDistr_bind A C (SDistr_bind B C f ∙ g) = SDistr_bind B C f ∙ SDistr_bind A B g.
proof: Proof. intros A B C f g. simpl in f. simpl in g. simpl. apply boolp.funext. intro de. symmetry. apply distr_ext. intro c. simpl. apply dlet_dlet. Qed.
imports: Coq(Relation_Definitions Morphisms) mathcomp(all_ssreflect all_algebra distr reals realsum) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) Crypt(ChoiceAsOrd Axioms)