proposition: Lemma kernel_normal : normal Ker.
proof: Proof. red in |- *. simpl in |- *. intros x y H'; try assumption. apply Trans with (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) x) (Ap (sgroup_map (monoid_sgroup_hom f)) (sgroup_law G y (group_inverse G x)))); auto with algebra. apply Trans with (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) x) (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) y) (Ap (sgroup_map (monoid_sgroup_hom f)) (group_inverse G x)))); auto with algebra. apply Trans with (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) x) (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) y) (group_inverse _ (Ap (sgroup_map (monoid_sgroup_hom f)) x)))); auto with algebra. apply Trans with (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) x) (sgroup_law _ (monoid_unit G') (group_inverse _ (Ap (sgroup_map (monoid_sgroup_hom f)) x)))); auto with algebra. apply Trans with (sgroup_law _ (Ap (sgroup_map (monoid_sgroup_hom f)) x) (group_inverse _ (Ap (sgroup_map (monoid_sgroup_hom f)) x))); auto with algebra. Qed.
imports: Group_util Group_quotient Parts2