proposition: Lemma operation_unit : forall s : S, Equal (op (monoid_unit M) s) s.
proof: Proof. intros s; try assumption. apply Trans with (Id S s); auto with algebra. cut (Equal (op (monoid_unit M)) (Id S)); auto with algebra. apply Trans with (monoid_unit (Endo_SET S)). generalize (monoid_hom_prf op). unfold monoid_hom_prop in |- *. auto with algebra. auto with algebra. Qed.
imports: Endo_set