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