proposition: Lemma operation_assoc : forall (x y : M) (s : S), Equal (op (sgroup_law _ x y) s) (op x (op y s)).
proof: Proof. intros x y s; try assumption. apply Trans with (Ap (sgroup_law (Endo_SET S) (Ap (sgroup_map (monoid_sgroup_hom op)) x) (Ap (sgroup_map (monoid_sgroup_hom op)) y)) s); auto with algebra. cut (Equal (op (sgroup_law _ x y)) (sgroup_law (Endo_SET S) (op x) (op y))). auto with algebra. apply (sgroup_hom_prf op). Qed.
imports: Endo_set