proposition: Lemma SGROUP_assoc : forall x y z : E, Equal (sgroup_law _ (sgroup_law _ x y) z) (sgroup_law _ x (sgroup_law _ y z)).
proof: Proof. intros x y z; try assumption. apply (sgroup_assoc_prf E x y z); auto with algebra. Qed.
imports: Sgroup_cat