proposition: Lemma mulIDl : left_distributive mulI addI.
proof: Proof. move=> ? ? ? ; apply sig_eq=> /=. by rewrite -mulrA [in t in (_ * t)]mulrC mulrA mulrDl. 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)