fact: Record monoid := mkMonoid { monoid_carrier :> Type ; monoid_unit : monoid_carrier ; monoid_mult : monoid_carrier -> monoid_carrier -> monoid_carrier ; monoid_law1 : forall m, monoid_mult monoid_unit m = m ; monoid_law2 : forall m, monoid_mult m monoid_unit = m ; monoid_law3 : forall m1 m2 m3, monoid_mult (monoid_mult m1 m2) m3 = monoid_mult m1 (monoid_mult m2 m3) }.
imports: Coq(ssreflect ssrfun ssrbool List) Coq(FunctionalExtensionality) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures)