proposition: Lemma surj_group_quo_ker_surjective : surjective surj_group_quo_ker.
proof: Proof. red in |- *. simpl in |- *. unfold group_quo_eq, subtype_image_equal in |- *. intros y; exists y; try assumption. simpl in |- *. apply Trans with (Ap (sgroup_map (monoid_sgroup_hom f)) (monoid_unit G)); auto with algebra. Qed.
imports: Group_kernel