proposition: Proposition projection_split_beta {B A : AbGroup} (E : AbSES B A) {s : B $-> E} (h : (projection _) $o s == idmap) : projection_split_iso E h o (inclusion _) == ab_biprod_inl.
proof: Proof. intro a. refine (ap _ (ab_corec_beta _ _ _ _) @ _). refine (ab_biprod_functor_beta _ _ _ _ _ @ _). nrapply path_prod'. 2: rapply cx_isexact. refine (ap _ (projection_split_to_kernel_beta E h a) @ _). apply eissect. Defined.
imports: Basics Types Truncations.Core HSet WildCat Groups.QuotientGroup Groups.ShortExactSequence AbelianGroup AbGroups.Biproduct AbHom Homotopy.ExactSequence Pointed Modalities.ReflectiveSubuniverse