fact: Record monoid_action (M : monoid) := mkAction { monact_carrier :> Type ; monact_action : M -> monact_carrier -> monact_carrier ; monact_unit : forall x, monact_action (e M) x = x ; monact_mult : forall m1 m2 x, monact_action (m1 ⋅ m2) x = monact_action m1 (monact_action m2 x) }.
imports: Coq(ssreflect ssrfun ssrbool List) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures)