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