proposition: Lemma self_commute (p1 p2 : ProbS) : commute (wopProb p1) (wopProb p2).
proof: Proof. rewrite /commute /wopProb; apply sig_eq=> /=. extensionality k; apply sig_eq=> /=. rewrite !mulrDr !mulrA. do 2 rewrite [((1 - _)* _)as t in t * _]mulrC. rewrite 2![(p1∙1 * _)as t in t * _]mulrC. rewrite -2!addrA [in t in _+t]addrA [in t in _ + (t + _)]addrC !addrA. do 2 f_equal. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads Monoid DijkstraMonadExamples) mathcomp(all_ssreflect all_algebra reals distr) Relational(Commutativity)