fact: Record monoid : Set := mkmonoid {u : M; o : M -> M -> M; point_assoc : forall a b c : M, o a (o b c) = o (o a b) c; u_neutral_l : forall a : M, o u a = a; u_neutral_r : forall a : M, o a u = a}.
imports: Arith Constants