proposition: Lemma ABELIAN_SGROUP_permute : forall x y z : S, Equal (sgroup_law _ x (sgroup_law _ y z)) (sgroup_law _ y (sgroup_law _ x z)).
proof: Proof. intros x y z; try assumption. apply Trans with (sgroup_law S (sgroup_law S x y) z); auto with algebra. apply Trans with (sgroup_law S (sgroup_law S y x) z); auto with algebra. apply SGROUP_comp; auto with algebra. apply ABELIAN_SGROUP_com. Qed.
imports: Abelian_group_cat Group_facts