proposition: Lemma GROUP_hom_prop : forall x : G, Equal (f (group_inverse _ x)) (group_inverse _ (f x)).
proof: Proof. intros x; try assumption. apply Sym. apply GROUP_law_inverse. apply Trans with (f (sgroup_law _ x (group_inverse _ x))); auto with algebra. apply Trans with (f (monoid_unit G)); auto with algebra. cut (Equal (sgroup_law G x (group_inverse _ x)) (monoid_unit G)). auto with algebra. apply GROUP_inverse_r. Qed.
imports: Group_cat Sgroup_facts Monoid_facts