fact: Definition SM := { f : M -> M | exists m, forall m', f m' = m ⋅ m'}.
imports: Coq(ssreflect ssrfun ssrbool List) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures)