proposition: Theorem factor_group_hom : Equal f (comp_hom inj_coKer_group (comp_hom bij_group_quo_ker_coKer surj_group_quo_ker)).
proof: Proof. simpl in |- *. unfold Map_eq in |- *. simpl in |- *. auto with algebra. Qed.
imports: Group_kernel