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