proposition: Lemma bij_group_quo_ker_coKer_bijective : bijective bij_group_quo_ker_coKer.
proof: Proof. red in |- *. split; [ try assumption | idtac ]. red in |- *. simpl in |- *. unfold group_quo_eq, subtype_image_equal in |- *. simpl in |- *. intros x y H'; try assumption. apply Trans with (sgroup_law G' (Ap (sgroup_map (monoid_sgroup_hom f)) x) (Ap (sgroup_map (monoid_sgroup_hom f)) (group_inverse G y))); auto with algebra. apply Trans with (sgroup_law G' (Ap (sgroup_map (monoid_sgroup_hom f)) x) (group_inverse _ (Ap (sgroup_map (monoid_sgroup_hom f)) y))); auto with algebra. apply Trans with (sgroup_law G' (Ap (sgroup_map (monoid_sgroup_hom f)) x) (group_inverse _ (Ap (sgroup_map (monoid_sgroup_hom f)) x))); auto with algebra. red in |- *. intros y; try assumption. elim y. intros y' subtype_prf; try assumption. elim subtype_prf. intros x H'; try assumption. elim H'; intros H'0 H'1; try exact H'0; clear H'. exists x; try assumption. Qed.
imports: Group_kernel