proposition: Lemma mulIDr : right_distributive mulI addI.
proof: Proof. move=> ? ? ? ; apply sig_eq=> /=; by rewrite mulrA mulrDr. 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)