Abelian Monoids

Now we introduce commutativity and add some results.

Definition is_CAbMonoid (G : CMonoid) := commutes (csg_op (c:=G)).

Record CAbMonoid : Type :=
{cam_crr :> CMonoid;
cam_proof : is_CAbMonoid cam_crr}.

Section AbMonoid_Axioms.

Variable M : CAbMonoid.

Let M be an abelian monoid.

Lemma CAbMonoid_is_CAbMonoid : is_CAbMonoid M.

Lemma cam_commutes : commutes (csg_op (c:=M)).

Lemma cam_commutes_unfolded : forall x y : M, x[+]y [=] y[+]x.

End AbMonoid_Axioms.

Section SubCAbMonoids.

Subgroups of an Abelian Monoid

Variable M : CAbMonoid.
Variable P : M -> CProp.
Variable Punit : P 0.
Variable op_pres_P : bin_op_pres_pred _ P csg_op.

Let M be an Abelian Monoid and P be a (CProp-valued) predicate on M that contains 0 and is closed under + and [--].