proposition: Lemma ABELIAN_MONOID_com : forall x y : M, Equal (sgroup_law _ x y) (sgroup_law _ y x).
proof: Proof. change (forall x y : M:ABELIAN_SGROUP, Equal (sgroup_law _ x y) (sgroup_law _ y x)) in |- *; auto with algebra. Qed.
imports: Abelian_group_cat Group_facts